nfcont_4.miz



    begin

    reserve n,m,i,k for Element of NAT ;

    reserve x,X,X1 for set;

    reserve r,p for Real;

    reserve s,x0,x1,x2 for Real;

    reserve f,f1,f2 for PartFunc of REAL , ( REAL n);

    reserve h for PartFunc of REAL , ( REAL-NS n);

    reserve W for non empty set;

    definition

      let n, f, x0;

      :: NFCONT_4:def1

      pred f is_continuous_in x0 means ex g be PartFunc of REAL , ( REAL-NS n) st f = g & g is_continuous_in x0;

    end

    theorem :: NFCONT_4:1

    h = f implies (f is_continuous_in x0 iff h is_continuous_in x0);

    theorem :: NFCONT_4:2

    

     Th2: x0 in X & f is_continuous_in x0 implies (f | X) is_continuous_in x0

    proof

      assume that

       A1: x0 in X and

       A2: f is_continuous_in x0;

      consider g be PartFunc of REAL , ( REAL-NS n) such that

       A3: f = g & g is_continuous_in x0 by A2;

      (g | X) is_continuous_in x0 by A1, A3, NFCONT_3: 6;

      hence thesis by A3;

    end;

    theorem :: NFCONT_4:3

    

     Th3: f is_continuous_in x0 iff x0 in ( dom f) & for r st 0 < r holds ex s st 0 < s & for x1 st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r

    proof

      hereby

        assume f is_continuous_in x0;

        then

        consider g be PartFunc of REAL , ( REAL-NS n) such that

         A1: f = g & g is_continuous_in x0;

        thus x0 in ( dom f) by A1;

        thus for r st 0 < r holds ex s st 0 < s & for x1 st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r

        proof

          let r;

          assume 0 < r;

          then

          consider s such that

           A2: 0 < s & for x1 st x1 in ( dom g) & |.(x1 - x0).| < s holds ||.((g /. x1) - (g /. x0)).|| < r by A1, NFCONT_3: 8;

          take s;

          thus 0 < s by A2;

          let x1;

          assume x1 in ( dom f) & |.(x1 - x0).| < s;

          then

           A3: ||.((g /. x1) - (g /. x0)).|| < r by A1, A2;

          (g /. x1) = (f /. x1) & (g /. x0) = (f /. x0) by A1, REAL_NS1:def 4;

          hence |.((f /. x1) - (f /. x0)).| < r by A3, REAL_NS1: 1, REAL_NS1: 5;

        end;

      end;

      assume

       A4: x0 in ( dom f) & for r st 0 < r holds ex s st 0 < s & for x1 st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r;

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      now

        let r be Real;

        reconsider rr = r as Real;

        assume 0 < r;

        then

        consider s such that

         A5: 0 < s and

         A6: for x1 st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < rr by A4;

        take s;

        thus 0 < s by A5;

        let x1;

        assume x1 in ( dom g) & |.(x1 - x0).| < s;

        then

         A7: |.((f /. x1) - (f /. x0)).| < r by A6;

        (g /. x1) = (f /. x1) & (g /. x0) = (f /. x0) by REAL_NS1:def 4;

        hence ||.((g /. x1) - (g /. x0)).|| < r by A7, REAL_NS1: 1, REAL_NS1: 5;

      end;

      then g is_continuous_in x0 by A4, NFCONT_3: 8;

      hence thesis;

    end;

    theorem :: NFCONT_4:4

    

     Th4: for r be Real, z be Element of ( REAL n), w be Point of ( REAL-NS n) st z = w holds { y where y be Element of ( REAL n) : |.(y - z).| < r } = { y where y be Point of ( REAL-NS n) : ||.(y - w).|| < r }

    proof

      let r be Real, z be Element of ( REAL n), w be Point of ( REAL-NS n);

      assume

       A1: z = w;

      set N1 = { y where y be Element of ( REAL n) : |.(y - z).| < r };

      set N2 = { y where y be Point of ( REAL-NS n) : ||.(y - w).|| < r };

      

       A2: N1 c= N2

      proof

        let x be object;

        assume x in N1;

        then

        consider y be Element of ( REAL n) such that

         A3: x = y & |.(y - z).| < r;

        reconsider x1 = x as Element of ( REAL n) by A3;

        reconsider x2 = x1 as Point of ( REAL-NS n) by REAL_NS1:def 4;

         ||.(x2 - w).|| < r by A1, A3, REAL_NS1: 1, REAL_NS1: 5;

        hence x in N2;

      end;

      N2 c= N1

      proof

        let x be object;

        assume x in N2;

        then

        consider y be Point of ( REAL-NS n) such that

         A4: x = y & ||.(y - w).|| < r;

        reconsider x3 = x as Point of ( REAL-NS n) by A4;

        reconsider x4 = x3 as Element of ( REAL n) by REAL_NS1:def 4;

         |.(x4 - z).| < r by A1, A4, REAL_NS1: 1, REAL_NS1: 5;

        hence x in N1;

      end;

      hence N1 = N2 by A2, XBOOLE_0:def 10;

    end;

    definition

      let n be Element of NAT ;

      let Z be set;

      let f be PartFunc of Z, ( REAL n);

      deffunc F( object) = |.(f /. $1).|;

      :: NFCONT_4:def2

      func |.f.| -> PartFunc of Z, REAL means

      : Def2: ( dom it ) = ( dom f) & for x be set st x in ( dom it ) holds (it /. x) = |.(f /. x).|;

      existence

      proof

        consider g be Function such that

         A1: ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) = F(x) from FUNCT_1:sch 3;

        now

          let y be object;

          assume y in ( rng g);

          then

          consider x be object such that

           A2: x in ( dom g) & y = (g . x) by FUNCT_1:def 3;

          (g . x) = F(x) by A1, A2;

          hence y in REAL by A2, XREAL_0:def 1;

        end;

        then ( rng g) c= REAL ;

        then g in ( PFuncs (Z, REAL )) by A1, PARTFUN1:def 3;

        then

        reconsider g as PartFunc of Z, REAL by PARTFUN1: 46;

        take g;

        thus ( dom g) = ( dom f) by A1;

        let x be set;

        assume

         A3: x in ( dom g);

        then (g . x) = F(x) by A1;

        hence thesis by A3, PARTFUN1:def 6;

      end;

      uniqueness

      proof

        let g1,g2 be PartFunc of Z, REAL such that

         A4: ( dom g1) = ( dom f) & for x be set st x in ( dom g1) holds (g1 /. x) = F(x) and

         A5: ( dom g2) = ( dom f) & for x be set st x in ( dom g2) holds (g2 /. x) = F(x);

        now

          let x be Element of Z;

          assume

           A6: x in ( dom g1);

          then

           A7: (g1 /. x) = |.(f /. x).| by A4;

          (g1 /. x) = (g2 /. x) by A5, A7, A4, A6;

          then (g1 . x) = (g2 /. x) by A6, PARTFUN1:def 6;

          hence (g1 . x) = (g2 . x) by A4, A5, A6, PARTFUN1:def 6;

        end;

        hence g1 = g2 by A4, A5, PARTFUN1: 5;

      end;

    end

    definition

      let n be Element of NAT ;

      let Z be non empty set;

      let f be PartFunc of Z, ( REAL n);

      deffunc G( set) = ( - (f /. $1));

      defpred P[ set] means $1 in ( dom f);

      :: NFCONT_4:def3

      func - f -> PartFunc of Z, ( REAL n) means

      : Def3: ( dom it ) = ( dom f) & for c be set st c in ( dom it ) holds (it /. c) = ( - (f /. c));

      existence

      proof

        consider F be PartFunc of Z, ( REAL n) such that

         A1: for c be Element of Z holds c in ( dom F) iff P[c] and

         A2: for c be Element of Z st c in ( dom F) holds (F /. c) = G(c) from PARTFUN2:sch 2;

        take F;

        thus thesis by A1, A2, SUBSET_1: 3;

      end;

      uniqueness

      proof

        let g1,g2 be PartFunc of Z, ( REAL n) such that

         A3: ( dom g1) = ( dom f) & for x be set st x in ( dom g1) holds (g1 /. x) = ( - (f /. x)) and

         A4: ( dom g2) = ( dom f) & for x be set st x in ( dom g2) holds (g2 /. x) = ( - (f /. x));

        now

          let x be Element of Z;

          assume

           A5: x in ( dom g1);

          then

           A6: (g1 /. x) = ( - (f /. x)) by A3;

          (g1 /. x) = (g2 /. x) by A4, A6, A3, A5;

          then (g1 . x) = (g2 /. x) by A5, PARTFUN1:def 6;

          hence (g1 . x) = (g2 . x) by A3, A4, A5, PARTFUN1:def 6;

        end;

        hence g1 = g2 by A3, A4, PARTFUN1: 5;

      end;

    end

    theorem :: NFCONT_4:5

    

     Th5: for f1,f2 be PartFunc of W, ( REAL-NS n), g1,g2 be PartFunc of W, ( REAL n) st f1 = g1 & f2 = g2 holds (f1 + f2) = (g1 + g2)

    proof

      let f1,f2 be PartFunc of W, ( REAL-NS n), g1,g2 be PartFunc of W, ( REAL n);

      assume

       A1: f1 = g1 & f2 = g2;

      

       A2: ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 1;

      then

       A3: ( dom (f1 + f2)) = ( dom (g1 + g2)) by A1, VALUED_2:def 45;

       A4:

      now

        let x be Element of W;

        assume

         A5: x in ( dom (f1 + f2));

        then

         A6: x in ( dom g1) & x in ( dom g2) by A2, A1, XBOOLE_0:def 4;

        

         A7: (f1 /. x) = (g1 /. x) & (f2 /. x) = (g2 /. x) by A1, REAL_NS1:def 4;

        (g1 /. x) = (g1 . x) & (g2 /. x) = (g2 . x) by A6, PARTFUN1:def 6;

        then

         A8: ((f1 /. x) + (f2 /. x)) = ((g1 . x) + (g2 . x)) by A7, REAL_NS1: 2;

        ((f1 + f2) /. x) = ((f1 /. x) + (f2 /. x)) by A5, VFUNCT_1:def 1;

        then ((f1 + f2) . x) = ((f1 /. x) + (f2 /. x)) by A5, PARTFUN1:def 6;

        hence ((f1 + f2) . x) = ((g1 + g2) . x) by A8, A3, A5, VALUED_2:def 45;

      end;

      (f1 + f2) is PartFunc of W, ( REAL n) by REAL_NS1:def 4;

      hence thesis by A3, A4, PARTFUN1: 5;

    end;

    theorem :: NFCONT_4:6

    

     Th6: for f1 be PartFunc of W, ( REAL-NS n), g1 be PartFunc of W, ( REAL n), a be Real st f1 = g1 holds (a (#) f1) = (a (#) g1)

    proof

      let f1 be PartFunc of W, ( REAL-NS n), g1 be PartFunc of W, ( REAL n), a be Real;

      assume

       A1: f1 = g1;

      

       A2: ( dom (a (#) f1)) = ( dom f1) by VFUNCT_1:def 4;

      then

       A3: ( dom (a (#) f1)) = ( dom (a (#) g1)) by A1, VALUED_2:def 39;

       A4:

      now

        let x be Element of W;

        assume

         A5: x in ( dom (a (#) f1));

        then

         A6: (g1 . x) = (g1 /. x) by A1, A2, PARTFUN1:def 6;

        (f1 /. x) = (g1 /. x) by A1, REAL_NS1:def 4;

        then

         A7: (a * (f1 /. x)) = (a * (g1 /. x)) by REAL_NS1: 3;

        

         A8: ((a (#) f1) /. x) = (a * (f1 /. x)) by A5, VFUNCT_1:def 4;

        ((a (#) g1) . x) = (a (#) (g1 . x)) by A3, A5, VALUED_2:def 39;

        hence ((a (#) f1) . x) = ((a (#) g1) . x) by A5, A7, A8, A6, PARTFUN1:def 6;

      end;

      (a (#) f1) is PartFunc of W, ( REAL n) by REAL_NS1:def 4;

      hence thesis by A3, A4, PARTFUN1: 5;

    end;

    theorem :: NFCONT_4:7

    for f1 be PartFunc of W, ( REAL n) holds (( - 1) (#) f1) = ( - f1)

    proof

      let f1 be PartFunc of W, ( REAL n);

      

       A1: ( dom (( - 1) (#) f1)) = ( dom f1) by VALUED_2:def 39;

      then

       A2: ( dom (( - 1) (#) f1)) = ( dom ( - f1)) by Def3;

      now

        let x be Element of W;

        assume

         A3: x in ( dom (( - 1) (#) f1));

        

         A4: (f1 . x) = (f1 /. x) by A1, A3, PARTFUN1:def 6;

        

         A5: (( - f1) /. x) = ( - (f1 /. x)) by A2, A3, Def3;

        ((f1 [#] ( - 1)) . x) = (( - 1) (#) (f1 . x)) by A3, VALUED_2:def 39;

        hence ((( - 1) (#) f1) . x) = (( - f1) . x) by A4, A2, A3, A5, PARTFUN1:def 6;

      end;

      hence thesis by A2, PARTFUN1: 5;

    end;

    theorem :: NFCONT_4:8

    

     Th8: for f1 be PartFunc of W, ( REAL-NS n), g1 be PartFunc of W, ( REAL n) st f1 = g1 holds ( - f1) = ( - g1)

    proof

      let f1 be PartFunc of W, ( REAL-NS n), g1 be PartFunc of W, ( REAL n);

      assume

       A1: f1 = g1;

      ( dom ( - f1)) = ( dom f1) by VFUNCT_1:def 5;

      then

       A2: ( dom ( - f1)) = ( dom ( - g1)) by A1, Def3;

       A3:

      now

        let x be Element of W;

        assume

         A4: x in ( dom ( - f1));

        (f1 /. x) = (g1 /. x) by A1, REAL_NS1:def 4;

        then

         A5: ( - (f1 /. x)) = ( - (g1 /. x)) by REAL_NS1: 4;

        

         A6: (( - f1) /. x) = ( - (f1 /. x)) by A4, VFUNCT_1:def 5;

        (( - g1) /. x) = ( - (g1 /. x)) by A2, A4, Def3;

        then (( - f1) . x) = (( - g1) /. x) by A4, A5, A6, PARTFUN1:def 6;

        hence (( - f1) . x) = (( - g1) . x) by A2, A4, PARTFUN1:def 6;

      end;

      ( - f1) is PartFunc of W, ( REAL n) by REAL_NS1:def 4;

      hence ( - f1) = ( - g1) by A2, A3, PARTFUN1: 5;

    end;

    theorem :: NFCONT_4:9

    

     Th9: for f1 be PartFunc of W, ( REAL-NS n), g1 be PartFunc of W, ( REAL n) st f1 = g1 holds ||.f1.|| = |.g1.|

    proof

      let f1 be PartFunc of W, ( REAL-NS n), g1 be PartFunc of W, ( REAL n);

      assume

       A1: f1 = g1;

      ( dom ||.f1.||) = ( dom f1) by NORMSP_0:def 3;

      then

       A2: ( dom ||.f1.||) = ( dom |.g1.|) by A1, Def2;

      now

        let x be Element of W;

        assume

         A3: x in ( dom ||.f1.||);

        

         A4: (f1 /. x) = (g1 /. x) by A1, REAL_NS1:def 4;

        set y1 = (g1 /. x);

        

         A5: ||.(f1 /. x).|| = |.y1.| by A4, REAL_NS1: 1;

        

         A6: ( ||.f1.|| . x) = ||.(f1 /. x).|| by A3, NORMSP_0:def 3;

        ( |.g1.| /. x) = |.(g1 /. x).| by A2, A3, Def2;

        hence ( ||.f1.|| . x) = ( |.g1.| . x) by A2, A3, A5, A6, PARTFUN1:def 6;

      end;

      hence thesis by A2, PARTFUN1: 5;

    end;

    theorem :: NFCONT_4:10

    

     Th10: for f1,f2 be PartFunc of W, ( REAL-NS n), g1,g2 be PartFunc of W, ( REAL n) st f1 = g1 & f2 = g2 holds (f1 - f2) = (g1 - g2)

    proof

      let f1,f2 be PartFunc of W, ( REAL-NS n), g1,g2 be PartFunc of W, ( REAL n);

      assume

       A1: f1 = g1 & f2 = g2;

      

       A2: ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) by VFUNCT_1:def 2;

      then

       A3: ( dom (f1 - f2)) = ( dom (g1 - g2)) by A1, VALUED_2:def 46;

       A4:

      now

        let x be Element of W;

        assume

         A5: x in ( dom (f1 - f2));

        

         A6: (f1 /. x) = (g1 /. x) & (f2 /. x) = (g2 /. x) by A1, REAL_NS1:def 4;

        x in ( dom f1) & x in ( dom f2) by A5, A2, XBOOLE_0:def 4;

        then (g1 . x) = (g1 /. x) & (g2 /. x) = (g2 . x) by A1, PARTFUN1:def 6;

        then

         A7: ((f1 /. x) - (f2 /. x)) = ((g1 . x) - (g2 . x)) by A6, REAL_NS1: 5;

        

         A8: ((f1 - f2) /. x) = ((f1 /. x) - (f2 /. x)) by A5, VFUNCT_1:def 2;

        ((f1 - f2) /. x) = ((f1 - f2) . x) by A5, PARTFUN1:def 6;

        hence ((f1 - f2) . x) = ((g1 - g2) . x) by A7, A8, A3, A5, VALUED_2:def 46;

      end;

      (f1 - f2) is PartFunc of W, ( REAL n) by REAL_NS1:def 4;

      hence (f1 - f2) = (g1 - g2) by A3, A4, PARTFUN1: 5;

    end;

    theorem :: NFCONT_4:11

    f is_continuous_in x0 iff x0 in ( dom f) & for N1 be Subset of ( REAL n) st ex r be Real st 0 < r & { y where y be Element of ( REAL n) : |.(y - (f /. x0)).| < r } = N1 holds ex N be Neighbourhood of x0 st for x1 st x1 in ( dom f) & x1 in N holds (f /. x1) in N1

    proof

      thus f is_continuous_in x0 implies x0 in ( dom f) & for N1 be Subset of ( REAL n) st ex r be Real st 0 < r & { y where y be Element of ( REAL n) : |.(y - (f /. x0)).| < r } = N1 holds ex N be Neighbourhood of x0 st for x1 st x1 in ( dom f) & x1 in N holds (f /. x1) in N1

      proof

        assume f is_continuous_in x0;

        then

        consider g be PartFunc of REAL , ( REAL-NS n) such that

         A1: f = g & g is_continuous_in x0;

        thus x0 in ( dom f) by A1;

        let N01 be Subset of ( REAL n) such that

         A2: ex r be Real st 0 < r & { y where y be Element of ( REAL n) : |.(y - (f /. x0)).| < r } = N01;

        consider r such that

         A3: 0 < r and

         A4: { p where p be Element of ( REAL n) : |.(p - (f /. x0)).| < r } = N01 by A2;

        (f /. x0) = (g /. x0) by A1, REAL_NS1:def 4;

        then

         A5: { p where p be Point of ( REAL-NS n) : ||.(p - (g /. x0)).|| < r } = N01 by A4, Th4;

        { p where p be Point of ( REAL-NS n) : ||.(p - (g /. x0)).|| < r } is Neighbourhood of (g /. x0) by A3, NFCONT_1: 3;

        then

        consider N be Neighbourhood of x0 such that

         A6: for x1 st x1 in ( dom g) & x1 in N holds (g /. x1) in N01 by A5, A1, NFCONT_3: 9;

        take N;

        let x1;

        assume x1 in ( dom f) & x1 in N;

        then (g /. x1) in N01 by A1, A6;

        hence (f /. x1) in N01 by A1, REAL_NS1:def 4;

      end;

      assume

       A7: x0 in ( dom f) & for N1 be Subset of ( REAL n) st ex r be Real st 0 < r & { y where y be Element of ( REAL n) : |.(y - (f /. x0)).| < r } = N1 holds ex N be Neighbourhood of x0 st for x1 st x1 in ( dom f) & x1 in N holds (f /. x1) in N1;

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      now

        let N1 be Neighbourhood of (g /. x0);

        consider r be Real such that

         A8: 0 < r and

         A9: { p where p be Point of ( REAL-NS n) : ||.(p - (g /. x0)).|| < r } c= N1 by NFCONT_1:def 1;

        reconsider rr = r as Real;

        

         A10: 0 < rr by A8;

        set N01 = { p where p be Element of ( REAL n) : |.(p - (f /. x0)).| < r };

        (f /. x0) = (g /. x0) by REAL_NS1:def 4;

        then

         A11: { p where p be Element of ( REAL n) : |.(p - (f /. x0)).| < r } = { p where p be Point of ( REAL-NS n) : ||.(p - (g /. x0)).|| < r } by Th4;

        now

          let x be object;

          assume x in N01;

          then ex p be Element of ( REAL n) st p = x & |.(p - (f /. x0)).| < r;

          hence x in ( REAL n);

        end;

        then N01 is Subset of ( REAL n) by TARSKI:def 3;

        then

        consider N be Neighbourhood of x0 such that

         A12: for x1 st x1 in ( dom f) & x1 in N holds (f /. x1) in N01 by A7, A10;

        take N;

        let x1;

        assume x1 in ( dom g) & x1 in N;

        then (f /. x1) in N01 by A12;

        then (g /. x1) in N01 by REAL_NS1:def 4;

        hence (g /. x1) in N1 by A9, A11;

      end;

      then g is_continuous_in x0 by A7, NFCONT_3: 9;

      hence thesis;

    end;

    theorem :: NFCONT_4:12

    f is_continuous_in x0 iff x0 in ( dom f) & for N1 be Subset of ( REAL n) st ex r be Real st 0 < r & { y where y be Element of ( REAL n) : |.(y - (f /. x0)).| < r } = N1 holds ex N be Neighbourhood of x0 st (f .: N) c= N1

    proof

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      hereby

        assume f is_continuous_in x0;

        then

         A1: g is_continuous_in x0;

        hence x0 in ( dom f);

        thus for N1 be Subset of ( REAL n) st ex r be Real st 0 < r & { y where y be Element of ( REAL n) : |.(y - (f /. x0)).| < r } = N1 holds ex N be Neighbourhood of x0 st (f .: N) c= N1

        proof

          let N1 be Subset of ( REAL n);

          given r be Real such that

           A2: 0 < r & { y where y be Element of ( REAL n) : |.(y - (f /. x0)).| < r } = N1;

          (f /. x0) = (g /. x0) by REAL_NS1:def 4;

          then

           A3: { p where p be Element of ( REAL n) : |.(p - (f /. x0)).| < r } = { p where p be Point of ( REAL-NS n) : ||.(p - (g /. x0)).|| < r } by Th4;

          N1 is Neighbourhood of (g /. x0) by A2, A3, NFCONT_1: 3;

          then

          consider N be Neighbourhood of x0 such that

           A4: (g .: N) c= N1 by A1, NFCONT_3: 10;

          take N;

          thus (f .: N) c= N1 by A4;

        end;

      end;

      assume

       A5: x0 in ( dom f) & for N1 be Subset of ( REAL n) st ex r be Real st 0 < r & { y where y be Element of ( REAL n) : |.(y - (f /. x0)).| < r } = N1 holds ex N be Neighbourhood of x0 st (f .: N) c= N1;

      now

        let N1 be Neighbourhood of (g /. x0);

        consider r be Real such that

         A6: 0 < r and

         A7: { p where p be Point of ( REAL-NS n) : ||.(p - (g /. x0)).|| < r } c= N1 by NFCONT_1:def 1;

        reconsider rr = r as Real;

        

         A8: 0 < rr by A6;

        set N01 = { p where p be Element of ( REAL n) : |.(p - (f /. x0)).| < r };

        (f /. x0) = (g /. x0) by REAL_NS1:def 4;

        then

         A9: { p where p be Element of ( REAL n) : |.(p - (f /. x0)).| < r } = { p where p be Point of ( REAL-NS n) : ||.(p - (g /. x0)).|| < r } by Th4;

        now

          let x be object;

          assume x in N01;

          then ex p be Element of ( REAL n) st p = x & |.(p - (f /. x0)).| < r;

          hence x in ( REAL n);

        end;

        then N01 is Subset of ( REAL n) by TARSKI:def 3;

        then

        consider N be Neighbourhood of x0 such that

         A10: (f .: N) c= N01 by A5, A8;

        take N;

        thus (g .: N) c= N1 by A7, A9, A10;

      end;

      then g is_continuous_in x0 by A5, NFCONT_3: 10;

      hence thesis;

    end;

    theorem :: NFCONT_4:13

    (ex N be Neighbourhood of x0 st (( dom f) /\ N) = {x0}) implies f is_continuous_in x0

    proof

      given N be Neighbourhood of x0 such that

       A1: (( dom f) /\ N) = {x0};

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      g is_continuous_in x0 by A1, NFCONT_3: 11;

      hence thesis;

    end;

    theorem :: NFCONT_4:14

    x0 in (( dom f1) /\ ( dom f2)) & f1 is_continuous_in x0 & f2 is_continuous_in x0 implies (f1 + f2) is_continuous_in x0

    proof

      assume

       A1: x0 in (( dom f1) /\ ( dom f2)) & f1 is_continuous_in x0 & f2 is_continuous_in x0;

      reconsider g1 = f1, g2 = f2 as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      

       A2: (g1 + g2) is_continuous_in x0 & (g1 - g2) is_continuous_in x0 by A1, NFCONT_3: 12;

      (g1 + g2) = (f1 + f2) by Th5;

      hence thesis by A2;

    end;

    theorem :: NFCONT_4:15

    x0 in (( dom f1) /\ ( dom f2)) & f1 is_continuous_in x0 & f2 is_continuous_in x0 implies (f1 - f2) is_continuous_in x0

    proof

      assume

       A1: x0 in (( dom f1) /\ ( dom f2)) & f1 is_continuous_in x0 & f2 is_continuous_in x0;

      reconsider g1 = f1, g2 = f2 as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      

       A2: (g1 + g2) is_continuous_in x0 & (g1 - g2) is_continuous_in x0 by A1, NFCONT_3: 12;

      (g1 - g2) = (f1 - f2) by Th10;

      hence thesis by A2;

    end;

    theorem :: NFCONT_4:16

    f is_continuous_in x0 implies (r (#) f) is_continuous_in x0

    proof

      assume

       A1: f is_continuous_in x0;

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      g is_continuous_in x0 by A1;

      then

       A2: (r (#) g) is_continuous_in x0 by NFCONT_3: 13;

      (r (#) g) = (r (#) f) by Th6;

      hence thesis by A2;

    end;

    theorem :: NFCONT_4:17

    x0 in ( dom f) & f is_continuous_in x0 implies |.f.| is_continuous_in x0

    proof

      assume

       A1: x0 in ( dom f) & f is_continuous_in x0;

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      g is_continuous_in x0 by A1;

      then ||.g.|| is_continuous_in x0 by NFCONT_3: 14;

      hence thesis by Th9;

    end;

    theorem :: NFCONT_4:18

    x0 in ( dom f) & f is_continuous_in x0 implies ( - f) is_continuous_in x0

    proof

      assume

       A1: x0 in ( dom f) & f is_continuous_in x0;

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      g is_continuous_in x0 by A1;

      then

       A2: ( - g) is_continuous_in x0 by NFCONT_3: 14;

      ( - g) = ( - f) by Th8;

      hence thesis by A2;

    end;

    theorem :: NFCONT_4:19

    for S be RealNormSpace, z be Point of ( REAL-NS n), f1 be PartFunc of REAL , ( REAL n), f2 be PartFunc of ( REAL-NS n), S st x0 in ( dom (f2 * f1)) & f1 is_continuous_in x0 & z = (f1 /. x0) & f2 is_continuous_in z holds (f2 * f1) is_continuous_in x0

    proof

      let S be RealNormSpace, z be Point of ( REAL-NS n), f1 be PartFunc of REAL , ( REAL n), f2 be PartFunc of ( REAL-NS n), S;

      assume

       A1: x0 in ( dom (f2 * f1)) & f1 is_continuous_in x0 & z = (f1 /. x0) & f2 is_continuous_in z;

      reconsider g1 = f1 as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      (f1 /. x0) = (g1 /. x0) by REAL_NS1:def 4;

      hence thesis by A1, NFCONT_3: 15;

    end;

    theorem :: NFCONT_4:20

    

     Th20: for S be RealNormSpace, f1 be PartFunc of REAL , S, f2 be PartFunc of S, REAL st x0 in ( dom (f2 * f1)) & f1 is_continuous_in x0 & f2 is_continuous_in (f1 /. x0) holds (f2 * f1) is_continuous_in x0

    proof

      let S be RealNormSpace, f1 be PartFunc of REAL , S, f2 be PartFunc of S, REAL ;

      assume

       A1: x0 in ( dom (f2 * f1));

      assume that

       A2: f1 is_continuous_in x0 and

       A3: f2 is_continuous_in (f1 /. x0);

      let s1 be Real_Sequence such that

       A4: ( rng s1) c= ( dom (f2 * f1)) and

       A5: s1 is convergent & ( lim s1) = x0;

      

       A6: ( dom (f2 * f1)) c= ( dom f1) by RELAT_1: 25;

      

       A7: ( rng (f1 /* s1)) c= ( dom f2)

      proof

        let x be object;

        assume x in ( rng (f1 /* s1));

        then

        consider n such that

         A8: x = ((f1 /* s1) . n) by FUNCT_2: 113;

        (s1 . n) in ( rng s1) by VALUED_0: 28;

        then (f1 . (s1 . n)) in ( dom f2) by A4, FUNCT_1: 11;

        hence x in ( dom f2) by A4, A6, A8, FUNCT_2: 108, XBOOLE_1: 1;

      end;

       A9:

      now

        let n;

        (s1 . n) in ( rng s1) by VALUED_0: 28;

        then

         A10: (s1 . n) in ( dom f1) by A4, FUNCT_1: 11;

        

        thus (((f2 * f1) /* s1) . n) = ((f2 * f1) . (s1 . n)) by A4, FUNCT_2: 108

        .= (f2 . (f1 . (s1 . n))) by A10, FUNCT_1: 13

        .= (f2 . ((f1 /* s1) . n)) by A4, A6, FUNCT_2: 108, XBOOLE_1: 1

        .= ((f2 /* (f1 /* s1)) . n) by A7, FUNCT_2: 108;

      end;

      then

       A11: (f2 /* (f1 /* s1)) = ((f2 * f1) /* s1) by FUNCT_2: 63;

      ( rng s1) c= ( dom f1) by A4, A6;

      then

       A12: (f1 /* s1) is convergent & (f1 /. x0) = ( lim (f1 /* s1)) by A2, A5;

      hence ((f2 * f1) /* s1) is convergent by A3, A7, A11, NFCONT_1:def 6;

      

      thus ((f2 * f1) . x0) = ((f2 * f1) /. x0) by A1, PARTFUN1:def 6

      .= (f2 /. (f1 /. x0)) by A1, PARTFUN2: 3

      .= ( lim (f2 /* (f1 /* s1))) by A12, A3, A7, NFCONT_1:def 6

      .= ( lim ((f2 * f1) /* s1)) by A9, FUNCT_2: 63;

    end;

    definition

      let n;

      let f be PartFunc of ( REAL n), REAL ;

      let x0 be Element of ( REAL n);

      :: NFCONT_4:def4

      pred f is_continuous_in x0 means ex y0 be Point of ( REAL-NS n), g be PartFunc of ( REAL-NS n), REAL st x0 = y0 & f = g & g is_continuous_in y0;

    end

    theorem :: NFCONT_4:21

    for f be PartFunc of ( REAL n), REAL , h be PartFunc of ( REAL-NS n), REAL , x0 be Element of ( REAL n), y0 be Point of ( REAL-NS n) st f = h & x0 = y0 holds f is_continuous_in x0 iff h is_continuous_in y0;

    theorem :: NFCONT_4:22

    

     Th22: for f1 be PartFunc of REAL , ( REAL n), f2 be PartFunc of ( REAL n), REAL st x0 in ( dom (f2 * f1)) & f1 is_continuous_in x0 & f2 is_continuous_in (f1 /. x0) holds (f2 * f1) is_continuous_in x0

    proof

      let f1 be PartFunc of REAL , ( REAL n), f2 be PartFunc of ( REAL n), REAL ;

      assume

       A1: x0 in ( dom (f2 * f1)) & f1 is_continuous_in x0 & f2 is_continuous_in (f1 /. x0);

      reconsider g1 = f1 as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      reconsider g2 = f2 as PartFunc of ( REAL-NS n), REAL by REAL_NS1:def 4;

      (f1 /. x0) = (g1 /. x0) by REAL_NS1:def 4;

      then g2 is_continuous_in (g1 /. x0) by A1;

      hence thesis by A1, Th20;

    end;

    definition

      let n, f;

      :: NFCONT_4:def5

      attr f is continuous means

      : Def5: for x0 st x0 in ( dom f) holds f is_continuous_in x0;

    end

    theorem :: NFCONT_4:23

    

     Th23: for g be PartFunc of REAL , ( REAL-NS n), f be PartFunc of REAL , ( REAL n) st g = f holds g is continuous iff f is continuous

    proof

      let g be PartFunc of REAL , ( REAL-NS n), f be PartFunc of REAL , ( REAL n);

      assume

       A1: g = f;

      hereby

        assume g is continuous;

        then for x0 st x0 in ( dom f) holds f is_continuous_in x0 by A1;

        hence f is continuous;

      end;

      assume

       A2: f is continuous;

      now

        let x0;

        assume x0 in ( dom g);

        then f is_continuous_in x0 by A2, A1;

        hence g is_continuous_in x0 by A1;

      end;

      hence thesis;

    end;

    theorem :: NFCONT_4:24

    

     Th24: X c= ( dom f) implies ((f | X) is continuous iff for x0, r st x0 in X & 0 < r holds ex s st 0 < s & for x1 st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r)

    proof

      assume

       A1: X c= ( dom f);

      thus (f | X) is continuous implies for x0, r st x0 in X & 0 < r holds ex s st 0 < s & for x1 st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r

      proof

        assume

         A2: (f | X) is continuous;

        let x0, r;

        assume that

         A3: x0 in X and

         A4: 0 < r;

        x0 in ( dom (f | X)) by A1, A3, RELAT_1: 62;

        then (f | X) is_continuous_in x0 by A2;

        then

        consider s such that

         A5: 0 < s and

         A6: for x1 st x1 in ( dom (f | X)) & |.(x1 - x0).| < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A4, Th3;

        take s;

        thus 0 < s by A5;

        let x1;

        assume that

         A7: x1 in X and

         A8: |.(x1 - x0).| < s;

        

         A9: ( dom (f | X)) = (( dom f) /\ X) by RELAT_1: 61

        .= X by A1, XBOOLE_1: 28;

        

        then |.((f /. x1) - (f /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A7, PARTFUN2: 15

        .= |.(((f | X) /. x1) - ((f | X) /. x0)).| by A3, A9, PARTFUN2: 15;

        hence thesis by A6, A9, A7, A8;

      end;

      assume

       A10: for x0, r st x0 in X & 0 < r holds ex s st 0 < s & for x1 st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r;

      

       A11: ( dom (f | X)) = (( dom f) /\ X) by RELAT_1: 61

      .= X by A1, XBOOLE_1: 28;

      now

        let x0 such that

         A12: x0 in ( dom (f | X));

        

         A13: x0 in X by A12, RELAT_1: 57;

        for r st 0 < r holds ex s st 0 < s & for x1 st x1 in ( dom (f | X)) & |.(x1 - x0).| < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r

        proof

          let r;

          assume 0 < r;

          then

          consider s such that

           A14: 0 < s and

           A15: for x1 st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r by A10, A13;

          take s;

          thus 0 < s by A14;

          let x1 such that

           A16: x1 in ( dom (f | X)) and

           A17: |.(x1 - x0).| < s;

           |.(((f | X) /. x1) - ((f | X) /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A12, PARTFUN2: 15

          .= |.((f /. x1) - (f /. x0)).| by A16, PARTFUN2: 15;

          hence thesis by A11, A15, A16, A17;

        end;

        hence (f | X) is_continuous_in x0 by Th3, A12;

      end;

      hence thesis;

    end;

    registration

      let n;

      cluster constant -> continuous for PartFunc of REAL , ( REAL n);

      coherence

      proof

        let f be PartFunc of REAL , ( REAL n);

        assume

         A1: f is constant;

        now

          reconsider s = 1 as Real;

          let x0, r;

          assume that

           A2: x0 in ( dom f) and

           A3: 0 < r;

          take s;

          thus 0 < s;

          let x1;

          assume

           A4: x1 in ( dom f);

          assume |.(x1 - x0).| < s;

          (f /. x1) = (f . x1) by A4, PARTFUN1:def 6

          .= (f . x0) by A1, A2, A4, FUNCT_1:def 10

          .= (f /. x0) by A2, PARTFUN1:def 6;

          hence |.((f /. x1) - (f /. x0)).| < r by A3;

        end;

        then (f | ( dom f)) is continuous by Th24;

        hence thesis by RELAT_1: 69;

      end;

    end

    registration

      let n;

      cluster continuous for PartFunc of REAL , ( REAL n);

      existence

      proof

        take f = the constant PartFunc of REAL , ( REAL n);

        thus thesis;

      end;

    end

    registration

      let n;

      let f be continuous PartFunc of REAL , ( REAL n), X be set;

      cluster (f | X) -> continuous;

      coherence

      proof

        for x0 st x0 in ( dom (f | X)) holds (f | X) is_continuous_in x0

        proof

          let x0;

          assume

           A1: x0 in ( dom (f | X));

          then x0 in ( dom f) by RELAT_1: 57;

          then

           A2: f is_continuous_in x0 by Def5;

          x0 in X by A1, RELAT_1: 57;

          hence thesis by A2, Th2;

        end;

        hence thesis;

      end;

    end

    theorem :: NFCONT_4:25

    (f | X) is continuous & X1 c= X implies (f | X1) is continuous

    proof

      assume

       A1: (f | X) is continuous;

      assume X1 c= X;

      then (f | X1) = ((f | X) | X1) by RELAT_1: 74;

      hence thesis by A1;

    end;

    registration

      let n;

      cluster empty -> continuous for PartFunc of REAL , ( REAL n);

      coherence ;

    end

    registration

      let n, f;

      let X be trivial set;

      cluster (f | X) -> continuous;

      coherence

      proof

        reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

        (g | X) is continuous PartFunc of REAL , ( REAL-NS n);

        hence thesis by Th23;

      end;

    end

    registration

      let n;

      let f1,f2 be continuous PartFunc of REAL , ( REAL n);

      cluster (f1 + f2) -> continuous;

      coherence

      proof

        reconsider g1 = f1, g2 = f2 as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

        

         A1: g1 is continuous & g2 is continuous by Th23;

        (g1 + g2) = (f1 + f2) by Th5;

        hence thesis by A1, Th23;

      end;

    end

    theorem :: NFCONT_4:26

    X c= (( dom f1) /\ ( dom f2)) & (f1 | X) is continuous & (f2 | X) is continuous implies ((f1 + f2) | X) is continuous & ((f1 - f2) | X) is continuous

    proof

      assume

       A1: X c= (( dom f1) /\ ( dom f2)) & (f1 | X) is continuous & (f2 | X) is continuous;

      reconsider g1 = f1, g2 = f2 as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      

       A2: (g1 | X) is continuous by A1, Th23;

      (g2 | X) is continuous by A1, Th23;

      then

       A3: ((g1 + g2) | X) is continuous & ((g1 - g2) | X) is continuous by A1, A2, NFCONT_3: 19;

      

       A4: (g1 + g2) = (f1 + f2) by Th5;

      (g1 - g2) = (f1 - f2) by Th10;

      hence thesis by A3, A4, Th23;

    end;

    theorem :: NFCONT_4:27

    X c= ( dom f1) & X1 c= ( dom f2) & (f1 | X) is continuous & (f2 | X1) is continuous implies ((f1 + f2) | (X /\ X1)) is continuous & ((f1 - f2) | (X /\ X1)) is continuous

    proof

      assume

       A1: X c= ( dom f1) & X1 c= ( dom f2) & (f1 | X) is continuous & (f2 | X1) is continuous;

      reconsider g1 = f1, g2 = f2 as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      

       A2: (g1 | X) is continuous by A1, Th23;

      (g2 | X1) is continuous by A1, Th23;

      then

       A3: ((g1 + g2) | (X /\ X1)) is continuous & ((g1 - g2) | (X /\ X1)) is continuous by A1, A2, NFCONT_3: 20;

      

       A4: (g1 + g2) = (f1 + f2) by Th5;

      (g1 - g2) = (f1 - f2) by Th10;

      hence thesis by A3, A4, Th23;

    end;

    registration

      let n;

      let f be continuous PartFunc of REAL , ( REAL n);

      let r;

      cluster (r (#) f) -> continuous;

      coherence

      proof

        reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

        

         A1: g is continuous by Th23;

        (r (#) g) = (r (#) f) by Th6;

        hence thesis by A1, Th23;

      end;

    end

    theorem :: NFCONT_4:28

    X c= ( dom f) & (f | X) is continuous implies ((r (#) f) | X) is continuous

    proof

      assume

       A1: X c= ( dom f) & (f | X) is continuous;

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      (g | X) is continuous PartFunc of REAL , ( REAL-NS n) by A1, Th23;

      then

       A2: ((r (#) g) | X) is continuous by A1, NFCONT_3: 21;

      (r (#) g) = (r (#) f) by Th6;

      hence thesis by A2, Th23;

    end;

    theorem :: NFCONT_4:29

    X c= ( dom f) & (f | X) is continuous implies ( |.f.| | X) is continuous & (( - f) | X) is continuous

    proof

      assume

       A1: X c= ( dom f) & (f | X) is continuous;

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      (g | X) is continuous by A1, Th23;

      then

       A2: ( ||.g.|| | X) is continuous & (( - g) | X) is continuous by A1, NFCONT_3: 22;

      hence ( |.f.| | X) is continuous by Th9;

      ( - g) = ( - f) by Th8;

      hence (( - f) | X) is continuous by A2, Th23;

    end;

    theorem :: NFCONT_4:30

    f is total & (for x1, x2 holds (f /. (x1 + x2)) = ((f /. x1) + (f /. x2))) & (ex x0 st f is_continuous_in x0) implies (f | REAL ) is continuous

    proof

      assume

       A1: f is total & (for x1, x2 holds (f /. (x1 + x2)) = ((f /. x1) + (f /. x2)));

      given x0 such that

       A2: f is_continuous_in x0;

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

       A3:

      now

        let x1, x2;

        

         A4: (g /. x1) = (f /. x1) & (g /. x2) = (f /. x2) by REAL_NS1:def 4;

        

        thus (g /. (x1 + x2)) = (f /. (x1 + x2)) by REAL_NS1:def 4

        .= ((f /. x1) + (f /. x2)) by A1

        .= ((g /. x1) + (g /. x2)) by A4, REAL_NS1: 2;

      end;

      g is_continuous_in x0 by A2;

      then (g | REAL ) is continuous by A1, A3, NFCONT_3: 23;

      hence thesis by Th23;

    end;

    theorem :: NFCONT_4:31

    for Y be Subset of ( REAL-NS n) st ( dom f) is compact & (f | ( dom f)) is continuous & Y = ( rng f) holds Y is compact

    proof

      let Y be Subset of ( REAL-NS n);

      assume

       A1: ( dom f) is compact & (f | ( dom f)) is continuous & Y = ( rng f);

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      (g | ( dom g)) is continuous by A1, Th23;

      hence Y is compact by A1, NFCONT_3: 24;

    end;

    theorem :: NFCONT_4:32

    for Y be Subset of REAL , Z be Subset of ( REAL-NS n) st Y c= ( dom f) & Z = (f .: Y) & Y is compact & (f | Y) is continuous holds Z is compact

    proof

      let Y be Subset of REAL , Z be Subset of ( REAL-NS n);

      assume

       A1: Y c= ( dom f) & Z = (f .: Y) & Y is compact & (f | Y) is continuous;

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      (g | Y) is continuous by A1, Th23;

      hence Z is compact by A1, NFCONT_3: 25;

    end;

    definition

      let n, f;

      :: NFCONT_4:def6

      attr f is Lipschitzian means ex g be PartFunc of REAL , ( REAL-NS n) st g = f & g is Lipschitzian;

    end

    theorem :: NFCONT_4:33

    

     Th33: f is Lipschitzian iff ex r be Real st 0 < r & for x1, x2 st x1 in ( dom f) & x2 in ( dom f) holds |.((f /. x1) - (f /. x2)).| <= (r * |.(x1 - x2).|)

    proof

      hereby

        assume f is Lipschitzian;

        then

        consider g be PartFunc of REAL , ( REAL-NS n) such that

         A1: g = f & g is Lipschitzian;

        consider r be Real such that

         A2: 0 < r & for x1, x2 st x1 in ( dom g) & x2 in ( dom g) holds ||.((g /. x1) - (g /. x2)).|| <= (r * |.(x1 - x2).|) by A1;

        take r;

        thus 0 < r by A2;

        thus for x1, x2 st x1 in ( dom f) & x2 in ( dom f) holds |.((f /. x1) - (f /. x2)).| <= (r * |.(x1 - x2).|)

        proof

          let x1, x2;

          assume x1 in ( dom f) & x2 in ( dom f);

          then

           A3: ||.((g /. x1) - (g /. x2)).|| <= (r * |.(x1 - x2).|) by A1, A2;

          (f /. x1) = (g /. x1) & (f /. x2) = (g /. x2) by A1, REAL_NS1:def 4;

          hence |.((f /. x1) - (f /. x2)).| <= (r * |.(x1 - x2).|) by A3, REAL_NS1: 1, REAL_NS1: 5;

        end;

      end;

      given r be Real such that

       A4: 0 < r & for x1, x2 st x1 in ( dom f) & x2 in ( dom f) holds |.((f /. x1) - (f /. x2)).| <= (r * |.(x1 - x2).|);

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      now

        let x1, x2;

        assume x1 in ( dom g) & x2 in ( dom g);

        then

         A5: |.((f /. x1) - (f /. x2)).| <= (r * |.(x1 - x2).|) by A4;

        (f /. x1) = (g /. x1) & (f /. x2) = (g /. x2) by REAL_NS1:def 4;

        hence ||.((g /. x1) - (g /. x2)).|| <= (r * |.(x1 - x2).|) by A5, REAL_NS1: 1, REAL_NS1: 5;

      end;

      then g is Lipschitzian by A4;

      hence thesis;

    end;

    theorem :: NFCONT_4:34

    

     Th34: f = h implies (f is Lipschitzian iff h is Lipschitzian);

    theorem :: NFCONT_4:35

    (f | X) is Lipschitzian iff ex r be Real st 0 < r & for x1, x2 st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) holds |.((f /. x1) - (f /. x2)).| <= (r * |.(x1 - x2).|)

    proof

      hereby

        assume (f | X) is Lipschitzian;

        then

        consider r be Real such that

         A1: 0 < r & for x1, x2 st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) holds |.(((f | X) /. x1) - ((f | X) /. x2)).| <= (r * |.(x1 - x2).|) by Th33;

        take r;

        thus 0 < r by A1;

        thus for x1, x2 st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) holds |.((f /. x1) - (f /. x2)).| <= (r * |.(x1 - x2).|)

        proof

          let x1, x2;

          assume

           A2: x1 in ( dom (f | X)) & x2 in ( dom (f | X));

          then |.(((f | X) /. x1) - ((f | X) /. x2)).| <= (r * |.(x1 - x2).|) by A1;

          then |.((f /. x1) - ((f | X) /. x2)).| <= (r * |.(x1 - x2).|) by A2, PARTFUN2: 15;

          hence |.((f /. x1) - (f /. x2)).| <= (r * |.(x1 - x2).|) by A2, PARTFUN2: 15;

        end;

      end;

      given r be Real such that

       A3: 0 < r & for x1, x2 st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) holds |.((f /. x1) - (f /. x2)).| <= (r * |.(x1 - x2).|);

      now

        let x1, x2;

        assume

         A4: x1 in ( dom (f | X)) & x2 in ( dom (f | X));

        then |.((f /. x1) - (f /. x2)).| <= (r * |.(x1 - x2).|) by A3;

        then |.(((f | X) /. x1) - (f /. x2)).| <= (r * |.(x1 - x2).|) by A4, PARTFUN2: 15;

        hence |.(((f | X) /. x1) - ((f | X) /. x2)).| <= (r * |.(x1 - x2).|) by A4, PARTFUN2: 15;

      end;

      hence (f | X) is Lipschitzian by A3, Th33;

    end;

    registration

      let n;

      cluster empty -> Lipschitzian for PartFunc of REAL , ( REAL n);

      coherence

      proof

        let f be PartFunc of REAL , ( REAL n);

        reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

        assume f is empty;

        then g is empty;

        hence thesis;

      end;

    end

    registration

      let n;

      cluster empty for PartFunc of REAL , ( REAL n);

      existence

      proof

        take the empty PartFunc of REAL , ( REAL n);

        thus thesis;

      end;

    end

    registration

      let n;

      let f be Lipschitzian PartFunc of REAL , ( REAL n), X be set;

      cluster (f | X) -> Lipschitzian;

      coherence

      proof

        reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

        g is Lipschitzian by Th34;

        then (g | X) is Lipschitzian;

        hence thesis;

      end;

    end

    theorem :: NFCONT_4:36

    (f | X) is Lipschitzian & X1 c= X implies (f | X1) is Lipschitzian

    proof

      assume that

       A1: (f | X) is Lipschitzian and

       A2: X1 c= X;

      (f | X1) = ((f | X) | X1) by A2, RELAT_1: 74;

      hence thesis by A1;

    end;

    registration

      let n;

      let f1,f2 be Lipschitzian PartFunc of REAL , ( REAL n);

      cluster (f1 + f2) -> Lipschitzian;

      coherence

      proof

        reconsider g1 = f1, g2 = f2 as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

        

         A1: g1 is Lipschitzian & g2 is Lipschitzian by Th34;

        (g1 + g2) = (f1 + f2) by Th5;

        hence thesis by A1;

      end;

      cluster (f1 - f2) -> Lipschitzian;

      coherence

      proof

        reconsider g1 = f1, g2 = f2 as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

        

         A2: g1 is Lipschitzian & g2 is Lipschitzian by Th34;

        (g1 - g2) = (f1 - f2) by Th10;

        hence thesis by A2;

      end;

    end

    theorem :: NFCONT_4:37

    (f1 | X) is Lipschitzian & (f2 | X1) is Lipschitzian implies ((f1 + f2) | (X /\ X1)) is Lipschitzian

    proof

      assume

       A1: (f1 | X) is Lipschitzian & (f2 | X1) is Lipschitzian;

      reconsider g1 = f1, g2 = f2 as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      (g1 | X) is Lipschitzian & (g2 | X1) is Lipschitzian by A1;

      then

       A2: ((g1 + g2) | (X /\ X1)) is Lipschitzian by NFCONT_3: 28;

      (g1 + g2) = (f1 + f2) by Th5;

      hence thesis by A2;

    end;

    theorem :: NFCONT_4:38

    (f1 | X) is Lipschitzian & (f2 | X1) is Lipschitzian implies ((f1 - f2) | (X /\ X1)) is Lipschitzian

    proof

      assume

       A1: (f1 | X) is Lipschitzian & (f2 | X1) is Lipschitzian;

      reconsider g1 = f1, g2 = f2 as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      (g1 | X) is Lipschitzian & (g2 | X1) is Lipschitzian by A1;

      then

       A2: ((g1 - g2) | (X /\ X1)) is Lipschitzian by NFCONT_3: 29;

      (g1 - g2) = (f1 - f2) by Th10;

      hence thesis by A2;

    end;

    registration

      let n;

      let f be Lipschitzian PartFunc of REAL , ( REAL n);

      let p;

      cluster (p (#) f) -> Lipschitzian;

      coherence

      proof

        reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

        

         A1: g is Lipschitzian by Th34;

        (p (#) g) = (p (#) f) by Th6;

        hence thesis by A1;

      end;

    end

    theorem :: NFCONT_4:39

    (f | X) is Lipschitzian & X c= ( dom f) implies ((p (#) f) | X) is Lipschitzian

    proof

      assume

       A1: (f | X) is Lipschitzian & X c= ( dom f);

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      

       A2: ((p (#) g) | X) is Lipschitzian by A1, NFCONT_3: 30;

      (p (#) g) = (p (#) f) by Th6;

      hence thesis by A2;

    end;

    registration

      let n;

      let f be Lipschitzian PartFunc of REAL , ( REAL n);

      cluster |.f.| -> Lipschitzian;

      coherence

      proof

        reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

        g is Lipschitzian by Th34;

        then ||.g.|| is Lipschitzian;

        hence thesis by Th9;

      end;

    end

    theorem :: NFCONT_4:40

    (f | X) is Lipschitzian implies ( - (f | X)) is Lipschitzian & ( |.f.| | X) is Lipschitzian & (( - f) | X) is Lipschitzian

    proof

      assume

       A1: (f | X) is Lipschitzian;

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      (g | X) is Lipschitzian by A1;

      then

       A2: ( - (g | X)) is Lipschitzian & ( ||.g.|| | X) is Lipschitzian & (( - g) | X) is Lipschitzian by NFCONT_3: 31;

      ( - (g | X)) = ( - (f | X)) by Th8;

      hence ( - (f | X)) is Lipschitzian by A2;

      thus ( |.f.| | X) is Lipschitzian by A2, Th9;

      ( - g) = ( - f) by Th8;

      hence thesis by A2;

    end;

    registration

      let n;

      cluster constant -> Lipschitzian for PartFunc of REAL , ( REAL n);

      coherence

      proof

        let f be PartFunc of REAL , ( REAL n);

        assume

         A1: f is constant;

        reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

        g is constant by A1;

        hence thesis;

      end;

    end

    registration

      let n;

      cluster Lipschitzian -> continuous for PartFunc of REAL , ( REAL n);

      coherence by Th23;

    end

    theorem :: NFCONT_4:41

    for r,p be Element of ( REAL n) st (for x0 st x0 in X holds (f /. x0) = ((x0 * r) + p)) holds (f | X) is continuous

    proof

      let r,p be Element of ( REAL n);

      assume

       A1: for x0 st x0 in X holds (f /. x0) = ((x0 * r) + p);

      reconsider g = f as PartFunc of REAL , ( REAL-NS n) by REAL_NS1:def 4;

      reconsider r0 = r, p0 = p as Point of ( REAL-NS n) by REAL_NS1:def 4;

      now

        let x0;

        assume

         A2: x0 in X;

        

         A3: (x0 * r) = (x0 * r0) by REAL_NS1: 3;

        

        thus (g /. x0) = (f /. x0) by REAL_NS1:def 4

        .= ((x0 * r) + p) by A2, A1

        .= ((x0 * r0) + p0) by A3, REAL_NS1: 2;

      end;

      then (g | X) is continuous by NFCONT_3: 33;

      hence thesis by Th23;

    end;

    theorem :: NFCONT_4:42

    

     Th42: for x0 be Element of ( REAL n) st 1 <= i & i <= n holds ( proj (i,n)) is_continuous_in x0

    proof

      let x0 be Element of ( REAL n);

      assume

       A1: 1 <= i & i <= n;

      

       A2: ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

      reconsider prg = ( proj (i,n)) as PartFunc of ( REAL-NS n), REAL by REAL_NS1:def 4;

      reconsider px0 = x0 as Element of ( REAL-NS n) by REAL_NS1:def 4;

      now

        let r be Real;

        assume

         A3: 0 < r;

        take s = r;

        thus 0 < s by A3;

        now

          let px1 be Element of ( REAL-NS n);

          assume

           A4: px1 in ( dom prg) & ||.(px1 - px0).|| < r;

          reconsider x1 = px1 as Element of ( REAL n) by REAL_NS1:def 4;

          

           A5: ||.(px1 - px0).|| = |.(x1 - x0).| by REAL_NS1: 1, REAL_NS1: 5;

          (( proj (i,n)) /. (x1 - x0)) = ((( proj (i,n)) /. x1) - (( proj (i,n)) /. x0)) by A1, PDIFF_8: 12;

          then |.((( proj (i,n)) /. x1) - (( proj (i,n)) /. x0)).| <= |.(x1 - x0).| by A1, PDIFF_8: 5;

          hence |.((( proj (i,n)) /. px1) - (( proj (i,n)) /. px0)).| < r by A4, A5, XXREAL_0: 2;

        end;

        hence for px1 be Element of ( REAL-NS n) st px1 in ( dom prg) & ||.(px1 - px0).|| < s holds |.((( proj (i,n)) /. px1) - (( proj (i,n)) /. px0)).| < r;

      end;

      then prg is_continuous_in px0 by A2, NFCONT_1: 8;

      hence thesis;

    end;

    theorem :: NFCONT_4:43

    

     Th43: for n be non zero Element of NAT , h be PartFunc of REAL , ( REAL n) holds h is_continuous_in x0 iff (x0 in ( dom h) & for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * h) is_continuous_in x0)

    proof

      let n be non zero Element of NAT , h be PartFunc of REAL , ( REAL n);

      hereby

        assume

         A1: h is_continuous_in x0;

        hence

         A2: x0 in ( dom h) by Th3;

        thus for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * h) is_continuous_in x0

        proof

          let i be Element of NAT ;

          assume i in ( Seg n);

          then

           A3: 1 <= i & i <= n by FINSEQ_1: 1;

          

           A4: ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

          ( rng h) c= ( REAL n);

          then

           A5: ( dom (( proj (i,n)) * h)) = ( dom h) by A4, RELAT_1: 27;

          ( proj (i,n)) is_continuous_in (h /. x0) by A3, Th42;

          hence thesis by A5, A1, A2, Th22;

        end;

      end;

      assume

       A6: x0 in ( dom h) & for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * h) is_continuous_in x0;

      for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Real st x1 in ( dom h) & |.(x1 - x0).| < s holds |.((h /. x1) - (h /. x0)).| < r

      proof

        let r0 be Real;

        assume

         A7: 0 < r0;

        set r = (r0 / 2);

        

         A8: 0 < r by A7, XREAL_1: 215;

        defpred P[ Nat, Real] means 0 < $2 & for x1 be Real st x1 in ( dom h) & |.(x1 - x0).| < $2 holds |.(((( proj ($1,n)) * h) . x1) - ((( proj ($1,n)) * h) . x0)).| < (r / n);

        

         A9: 0 < (r / n) by A8, XREAL_1: 139;

        

         A10: for j be Nat st j in ( Seg n) holds ex x be Element of REAL st P[j, x]

        proof

          let j be Nat;

          assume

           A11: j in ( Seg n);

          

           A12: (( proj (j,n)) * h) is_continuous_in x0 by A6, A11;

          

           A13: ( dom ( proj (j,n))) = ( REAL n) by FUNCT_2:def 1;

          ( rng h) c= ( REAL n);

          then

           A14: ( dom (( proj (j,n)) * h)) = ( dom h) by A13, RELAT_1: 27;

          consider sj be Real such that

           A15: 0 < sj & for x1 be Real st x1 in ( dom (( proj (j,n)) * h)) & |.(x1 - x0).| < sj holds |.(((( proj (j,n)) * h) . x1) - ((( proj (j,n)) * h) . x0)).| < (r / n) by A12, A9, FCONT_1: 3;

          sj in REAL by XREAL_0:def 1;

          hence thesis by A15, A14;

        end;

        consider s0 be FinSequence of REAL such that

         A16: ( dom s0) = ( Seg n) & for k be Nat st k in ( Seg n) holds P[k, (s0 . k)] from FINSEQ_1:sch 5( A10);

        n in ( Seg n) by FINSEQ_1: 3;

        then

        reconsider rs0 = ( rng s0) as non empty ext-real-membered set by A16, FUNCT_1: 3;

        ( rng s0) is finite by A16, FINSET_1: 8;

        then

        reconsider rs0 as left_end right_end non empty ext-real-membered set;

        

         A17: ( min rs0) in ( rng s0) by XXREAL_2:def 7;

        reconsider s = ( min rs0) as Real;

        take s;

        ex i1 be object st i1 in ( dom s0) & s = (s0 . i1) by A17, FUNCT_1:def 3;

        hence 0 < s by A16;

        now

          let x1;

          assume

           A18: x1 in ( dom h) & |.(x1 - x0).| < s;

          now

            let j be Element of NAT ;

            assume 1 <= j & j <= n;

            then

             A19: j in ( Seg n) by FINSEQ_1: 1;

            then (s0 . j) in ( rng s0) by A16, FUNCT_1: 3;

            then s <= (s0 . j) by XXREAL_2:def 7;

            then |.(x1 - x0).| < (s0 . j) by A18, XXREAL_0: 2;

            then

             A20: |.(((( proj (j,n)) * h) . x1) - ((( proj (j,n)) * h) . x0)).| < (r / n) by A19, A18, A16;

            

             A21: ((( proj (j,n)) * h) . x1) = (( proj (j,n)) . (h . x1)) by A18, FUNCT_1: 13

            .= (( proj (j,n)) . (h /. x1)) by A18, PARTFUN1:def 6;

            ((( proj (j,n)) * h) . x0) = (( proj (j,n)) . (h . x0)) by A6, FUNCT_1: 13

            .= (( proj (j,n)) . (h /. x0)) by A6, PARTFUN1:def 6;

            hence |.(( proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r / n) by A20, A21, PDIFF_8: 12;

          end;

          then |.((h /. x1) - (h /. x0)).| <= (n * (r / n)) by PDIFF_8: 17;

          then

           A22: |.((h /. x1) - (h /. x0)).| <= r by XCMPLX_1: 87;

          r < r0 by A7, XREAL_1: 216;

          hence |.((h /. x1) - (h /. x0)).| < r0 by A22, XXREAL_0: 2;

        end;

        hence for x1 st x1 in ( dom h) & |.(x1 - x0).| < s holds |.((h /. x1) - (h /. x0)).| < r0;

      end;

      hence thesis by A6, Th3;

    end;

    theorem :: NFCONT_4:44

    for n be non zero Element of NAT , h be PartFunc of REAL , ( REAL n) holds h is continuous iff for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * h) is continuous

    proof

      let n be non zero Element of NAT , h be PartFunc of REAL , ( REAL n);

      hereby

        assume

         A1: h is continuous;

        thus for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * h) is continuous

        proof

          let i be Element of NAT ;

          assume

           A2: i in ( Seg n);

          

           A3: ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

          ( rng h) c= ( REAL n);

          then

           A4: ( dom (( proj (i,n)) * h)) = ( dom h) by A3, RELAT_1: 27;

          now

            let x0;

            assume x0 in ( dom (( proj (i,n)) * h));

            then h is_continuous_in x0 by A1, A4;

            hence (( proj (i,n)) * h) is_continuous_in x0 by A2, Th43;

          end;

          hence (( proj (i,n)) * h) is continuous;

        end;

      end;

      assume

       A5: for i be Element of NAT st i in ( Seg n) holds (( proj (i,n)) * h) is continuous;

      let x0;

      assume

       A6: x0 in ( dom h);

      now

        let i be Element of NAT ;

        assume

         A7: i in ( Seg n);

        

         A8: ( dom ( proj (i,n))) = ( REAL n) by FUNCT_2:def 1;

        ( rng h) c= ( REAL n);

        then

         A9: ( dom (( proj (i,n)) * h)) = ( dom h) by A8, RELAT_1: 27;

        (( proj (i,n)) * h) is continuous by A5, A7;

        hence (( proj (i,n)) * h) is_continuous_in x0 by A6, A9;

      end;

      hence thesis by A6, Th43;

    end;

    theorem :: NFCONT_4:45

    

     Th45: for x0 be Point of ( REAL-NS n) st 1 <= i & i <= n holds ( Proj (i,n)) is_continuous_in x0

    proof

      let x0 be Point of ( REAL-NS n);

      assume

       A1: 1 <= i & i <= n;

      

       A2: ( dom ( Proj (i,n))) = the carrier of ( REAL-NS n) by FUNCT_2:def 1;

      now

        let r be Real;

        assume

         A3: 0 < r;

        take s = r;

        thus 0 < s by A3;

        now

          let x1 be Point of ( REAL-NS n);

          assume

           A4: x1 in ( dom ( Proj (i,n))) & ||.(x1 - x0).|| < s;

          (( Proj (i,n)) /. (x1 - x0)) = ((( Proj (i,n)) /. x1) - (( Proj (i,n)) /. x0)) by A1, PDIFF_8: 11;

          then ||.((( Proj (i,n)) /. x1) - (( Proj (i,n)) /. x0)).|| <= ||.(x1 - x0).|| by A1, PDIFF_8: 3;

          hence ||.((( Proj (i,n)) /. x1) - (( Proj (i,n)) /. x0)).|| < r by A4, XXREAL_0: 2;

        end;

        hence for x1 be Point of ( REAL-NS n) st x1 in ( dom ( Proj (i,n))) & ||.(x1 - x0).|| < s holds ||.((( Proj (i,n)) /. x1) - (( Proj (i,n)) /. x0)).|| < r;

      end;

      hence thesis by A2, NFCONT_1: 7;

    end;

    theorem :: NFCONT_4:46

    

     Th46: for n be non zero Element of NAT , h be PartFunc of REAL , ( REAL-NS n) holds h is_continuous_in x0 iff for i be Element of NAT st i in ( Seg n) holds (( Proj (i,n)) * h) is_continuous_in x0

    proof

      let n be non zero Element of NAT , h be PartFunc of REAL , ( REAL-NS n);

      hereby

        assume

         A1: h is_continuous_in x0;

        thus for i be Element of NAT st i in ( Seg n) holds (( Proj (i,n)) * h) is_continuous_in x0

        proof

          let i be Element of NAT ;

          assume i in ( Seg n);

          then

           A2: 1 <= i & i <= n by FINSEQ_1: 1;

          

           A3: ( dom ( Proj (i,n))) = the carrier of ( REAL-NS n) by FUNCT_2:def 1;

          ( rng h) c= the carrier of ( REAL-NS n);

          then

           A4: ( dom (( Proj (i,n)) * h)) = ( dom h) by A3, RELAT_1: 27;

          ( Proj (i,n)) is_continuous_in (h /. x0) by A2, Th45;

          hence (( Proj (i,n)) * h) is_continuous_in x0 by A4, A1, NFCONT_3: 15;

        end;

      end;

      assume

       A5: for i be Element of NAT st i in ( Seg n) holds (( Proj (i,n)) * h) is_continuous_in x0;

      1 <= n by NAT_1: 14;

      then 1 in ( Seg n) by FINSEQ_1: 1;

      then (( Proj (1,n)) * h) is_continuous_in x0 by A5;

      then

       A6: x0 in ( dom (( Proj (1,n)) * h));

      

       A7: ( dom (( Proj (1,n)) * h)) c= ( dom h) by RELAT_1: 25;

      for r be Real st 0 < r holds ex s st 0 < s & for x1 st x1 in ( dom h) & |.(x1 - x0).| < s holds ||.((h /. x1) - (h /. x0)).|| < r

      proof

        let r0 be Real;

        set r = (r0 / 2);

        assume

         A8: 0 < r0;

        then

         A9: 0 < r by XREAL_1: 215;

        defpred P[ set, Real] means ex j be Element of NAT st $1 = j & 0 < $2 & for x1 st x1 in ( dom h) & |.(x1 - x0).| < $2 holds ||.(((( Proj (j,n)) * h) /. x1) - ((( Proj (j,n)) * h) /. x0)).|| < (r / n);

        

         A10: 0 < (r / n) by A9, XREAL_1: 139;

        

         A11: for j0 be Nat st j0 in ( Seg n) holds ex x be Element of REAL st P[j0, x]

        proof

          let j0 be Nat;

          assume

           A12: j0 in ( Seg n);

          reconsider j = j0 as Element of NAT by ORDINAL1:def 12;

          

           A13: (( Proj (j,n)) * h) is_continuous_in x0 by A5, A12;

          

           A14: ( dom ( Proj (j,n))) = the carrier of ( REAL-NS n) by FUNCT_2:def 1;

          ( rng h) c= the carrier of ( REAL-NS n);

          then

           A15: ( dom (( Proj (j,n)) * h)) = ( dom h) by A14, RELAT_1: 27;

          consider sj be Real such that

           A16: 0 < sj & for x1 st x1 in ( dom (( Proj (j,n)) * h)) & |.(x1 - x0).| < sj holds ||.(((( Proj (j,n)) * h) /. x1) - ((( Proj (j,n)) * h) /. x0)).|| < (r / n) by A13, A10, NFCONT_3: 8;

          sj in REAL by XREAL_0:def 1;

          hence thesis by A16, A15;

        end;

        consider s0 be FinSequence of REAL such that

         A17: ( dom s0) = ( Seg n) & for k be Nat st k in ( Seg n) holds P[k, (s0 . k)] from FINSEQ_1:sch 5( A11);

        n in ( Seg n) by FINSEQ_1: 3;

        then

        reconsider rs0 = ( rng s0) as non empty ext-real-membered set by A17, FUNCT_1: 3;

        ( rng s0) is finite by A17, FINSET_1: 8;

        then

        reconsider rs0 as left_end right_end non empty ext-real-membered set;

        

         A18: ( min rs0) in ( rng s0) by XXREAL_2:def 7;

        reconsider s = ( min rs0) as Real;

        take s;

        consider i1 be object such that

         A19: i1 in ( dom s0) & s = (s0 . i1) by A18, FUNCT_1:def 3;

        ex j be Element of NAT st i1 = j & 0 < (s0 . i1) & for x1 st x1 in ( dom h) & |.(x1 - x0).| < (s0 . i1) holds ||.(((( Proj (j,n)) * h) /. x1) - ((( Proj (j,n)) * h) /. x0)).|| < (r / n) by A17, A19;

        hence 0 < s by A19;

        let x1;

        assume

         A20: x1 in ( dom h) & |.(x1 - x0).| < s;

        now

          let j be Element of NAT ;

          assume 1 <= j & j <= n;

          then

           A21: j in ( Seg n) by FINSEQ_1: 1;

          then

          consider jj be Element of NAT such that

           A22: jj = j & 0 < (s0 . j) & for x1 st x1 in ( dom h) & |.(x1 - x0).| < (s0 . j) holds ||.(((( Proj (jj,n)) * h) /. x1) - ((( Proj (jj,n)) * h) /. x0)).|| < (r / n) by A17;

          (s0 . j) in ( rng s0) by A21, A17, FUNCT_1: 3;

          then s <= (s0 . j) by XXREAL_2:def 7;

          then |.(x1 - x0).| < (s0 . j) by A20, XXREAL_0: 2;

          then

           A23: ||.(((( Proj (j,n)) * h) /. x1) - ((( Proj (j,n)) * h) /. x0)).|| < (r / n) by A22, A20;

          

           A24: ( dom ( Proj (j,n))) = the carrier of ( REAL-NS n) by FUNCT_2:def 1;

          then

           A25: ((( Proj (j,n)) * h) /. x1) = (( Proj (j,n)) /. (h /. x1)) by A20, PARTFUN2: 4;

          ((( Proj (j,n)) * h) /. x0) = (( Proj (j,n)) /. (h /. x0)) by A24, A7, A6, PARTFUN2: 4;

          hence ||.(( Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r / n) by A23, A25, PDIFF_8: 11;

        end;

        then ||.((h /. x1) - (h /. x0)).|| <= (n * (r / n)) by PDIFF_8: 16;

        then

         A26: ||.((h /. x1) - (h /. x0)).|| <= r by XCMPLX_1: 87;

        r < r0 by A8, XREAL_1: 216;

        hence ||.((h /. x1) - (h /. x0)).|| < r0 by A26, XXREAL_0: 2;

      end;

      hence thesis by A7, A6, NFCONT_3: 8;

    end;

    theorem :: NFCONT_4:47

    for n be non zero Element of NAT , h be PartFunc of REAL , ( REAL-NS n) holds h is continuous iff for i be Element of NAT st i in ( Seg n) holds (( Proj (i,n)) * h) is continuous

    proof

      let n be non zero Element of NAT , h be PartFunc of REAL , ( REAL-NS n);

      hereby

        assume

         A1: h is continuous;

        thus for i be Element of NAT st i in ( Seg n) holds (( Proj (i,n)) * h) is continuous

        proof

          let i be Element of NAT ;

          assume

           A2: i in ( Seg n);

          

           A3: ( dom ( Proj (i,n))) = the carrier of ( REAL-NS n) by FUNCT_2:def 1;

          ( rng h) c= the carrier of ( REAL-NS n);

          then

           A4: ( dom (( Proj (i,n)) * h)) = ( dom h) by A3, RELAT_1: 27;

          for x0 st x0 in ( dom (( Proj (i,n)) * h)) holds (( Proj (i,n)) * h) is_continuous_in x0 by A2, Th46, A1, A4;

          hence (( Proj (i,n)) * h) is continuous;

        end;

      end;

      assume

       A5: for i be Element of NAT st i in ( Seg n) holds (( Proj (i,n)) * h) is continuous;

      let x0;

      assume

       A6: x0 in ( dom h);

      now

        let i be Element of NAT ;

        assume

         A7: i in ( Seg n);

        

         A8: ( dom ( Proj (i,n))) = the carrier of ( REAL-NS n) by FUNCT_2:def 1;

        ( rng h) c= the carrier of ( REAL-NS n);

        then

         A9: ( dom (( Proj (i,n)) * h)) = ( dom h) by A8, RELAT_1: 27;

        (( Proj (i,n)) * h) is continuous by A5, A7;

        hence (( Proj (i,n)) * h) is_continuous_in x0 by A6, A9;

      end;

      hence h is_continuous_in x0 by Th46;

    end;