nfcont_1.miz



    begin

    reserve n,m for Nat;

    reserve x,X,X1 for set;

    reserve s,g,r,p for Real;

    reserve S,T for RealNormSpace;

    reserve f,f1,f2 for PartFunc of S, T;

    reserve s1,s2 for sequence of S;

    reserve x0,x1,x2 for Point of S;

    reserve Y for Subset of S;

    theorem :: NFCONT_1:1

    for S be non empty addLoopStr holds for seq1,seq2 be sequence of S holds (seq1 - seq2) = (seq1 + ( - seq2))

    proof

      let S be non empty addLoopStr;

      let seq1,seq2 be sequence of S;

      for n be Element of NAT holds ((seq1 - seq2) . n) = ((seq1 + ( - seq2)) . n)

      proof

        let n be Element of NAT ;

        

        thus ((seq1 - seq2) . n) = ((seq1 . n) - (seq2 . n)) by NORMSP_1:def 3

        .= ((seq1 . n) + (( - seq2) . n)) by BHSP_1: 44

        .= ((seq1 + ( - seq2)) . n) by NORMSP_1:def 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: NFCONT_1:2

    

     Th2: for seq be sequence of S holds ( - seq) = (( - 1) * seq)

    proof

      let seq be sequence of S;

      now

        let n be Element of NAT ;

        

        thus ((( - 1) * seq) . n) = (( - 1) * (seq . n)) by NORMSP_1:def 5

        .= ( - (seq . n)) by RLVECT_1: 16

        .= (( - seq) . n) by BHSP_1: 44;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    definition

      let S, x0;

      :: NFCONT_1:def1

      mode Neighbourhood of x0 -> Subset of S means

      : Def1: ex g be Real st 0 < g & { y where y be Point of S : ||.(y - x0).|| < g } c= it ;

      existence

      proof

        set N = { y where y be Point of S : ||.(y - x0).|| < 1 };

        take N;

        N c= the carrier of S

        proof

          let x be object;

          assume x in { y where y be Point of S : ||.(y - x0).|| < 1 };

          then ex y be Point of S st x = y & ||.(y - x0).|| < 1;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: NFCONT_1:3

    

     Th3: for g be Real st 0 < g holds { y where y be Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0

    proof

      let g be Real such that

       A1: g > 0 ;

      set N = { y where y be Point of S : ||.(y - x0).|| < g };

      N c= the carrier of S

      proof

        let x be object;

        assume x in { y where y be Point of S : ||.(y - x0).|| < g };

        then ex y be Point of S st x = y & ||.(y - x0).|| < g;

        hence thesis;

      end;

      hence thesis by A1, Def1;

    end;

    theorem :: NFCONT_1:4

    

     Th4: for N be Neighbourhood of x0 holds x0 in N

    proof

      let N be Neighbourhood of x0;

      consider g be Real such that

       A1: 0 < g and

       A2: { z where z be Point of S : ||.(z - x0).|| < g } c= N by Def1;

       ||.(x0 - x0).|| = ||.( 0. S).|| by RLVECT_1: 15

      .= 0 by NORMSP_1: 1;

      then x0 in { z where z be Point of S : ||.(z - x0).|| < g } by A1;

      hence thesis by A2;

    end;

    definition

      let S;

      let X be Subset of S;

      :: NFCONT_1:def2

      attr X is compact means for s1 be sequence of S st ( rng s1) c= X holds ex s2 be sequence of S st s2 is subsequence of s1 & s2 is convergent & ( lim s2) in X;

    end

    definition

      let S;

      let X be Subset of S;

      :: NFCONT_1:def3

      attr X is closed means for s1 be sequence of S st ( rng s1) c= X & s1 is convergent holds ( lim s1) in X;

    end

    definition

      let S;

      let X be Subset of S;

      :: NFCONT_1:def4

      attr X is open means (X ` ) is closed;

    end

    definition

      let S, T;

      let f, x0;

      :: NFCONT_1:def5

      pred f is_continuous_in x0 means x0 in ( dom f) & for s1 st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1));

    end

    definition

      let S;

      let f be PartFunc of the carrier of S, REAL ;

      let x0;

      :: NFCONT_1:def6

      pred f is_continuous_in x0 means x0 in ( dom f) & for s1 st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1));

    end

    theorem :: NFCONT_1:5

    

     Th5: for seq be sequence of S, h be PartFunc of S, T st ( rng seq) c= ( dom h) holds (seq . n) in ( dom h)

    proof

      let seq be sequence of S;

      

       A1: n in NAT by ORDINAL1:def 12;

      ( dom seq) = NAT by FUNCT_2:def 1;

      then (seq . n) in ( rng seq) by FUNCT_1:def 3, A1;

      hence thesis;

    end;

    theorem :: NFCONT_1:6

    

     Th6: for seq be sequence of S, x be set holds x in ( rng seq) iff ex n st x = (seq . n)

    proof

      let seq be sequence of S;

      let x be set;

      thus x in ( rng seq) implies ex n st x = (seq . n)

      proof

        assume x in ( rng seq);

        then

        consider y be object such that

         A1: y in ( dom seq) and

         A2: x = (seq . y) by FUNCT_1:def 3;

        reconsider m = y as Nat by A1;

        take m;

        thus thesis by A2;

      end;

      given n such that

       A3: x = (seq . n);

      n in NAT by ORDINAL1:def 12;

      then n in ( dom seq) by FUNCT_2:def 1;

      hence thesis by A3, FUNCT_1:def 3;

    end;

    theorem :: NFCONT_1:7

    

     Th7: 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

      thus f is_continuous_in x0 implies 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

        assume

         A1: f is_continuous_in x0;

        hence x0 in ( dom f);

        given r such that

         A2: 0 < r and

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

        reconsider r as Real;

        defpred P[ Nat, Point of S] means $2 in ( dom f) & ||.($2 - x0).|| < (1 / ($1 + 1)) & not ||.((f /. $2) - (f /. x0)).|| < r;

        

         A4: for n be Element of NAT holds ex p be Point of S st P[n, p]

        proof

          let n be Element of NAT ;

           0 < ((n + 1) " );

          then 0 < (1 / (n + 1)) by XCMPLX_1: 215;

          then

          consider p be Point of S such that

           A5: p in ( dom f) & ||.(p - x0).|| < (1 / (n + 1)) & not ||.((f /. p) - (f /. x0)).|| < r by A3;

          take p;

          thus thesis by A5;

        end;

        consider s1 be sequence of S such that

         A6: for n be Element of NAT holds P[n, (s1 . n)] from FUNCT_2:sch 3( A4);

        reconsider s1 as sequence of S;

        

         A7: ( rng s1) c= ( dom f)

        proof

          

           A8: ( dom s1) = NAT by FUNCT_2:def 1;

          let v be object;

          assume v in ( rng s1);

          then ex n be object st n in NAT & v = (s1 . n) by A8, FUNCT_1:def 3;

          hence thesis by A6;

        end;

         A9:

        now

          let n;

          

           A10: n in NAT by ORDINAL1:def 12;

           not ||.((f /. (s1 . n)) - (f /. x0)).|| < r by A6, A10;

          hence not ||.(((f /* s1) . n) - (f /. x0)).|| < r by A7, FUNCT_2: 109, A10;

        end;

         A11:

        now

          let s be Real;

          consider n be Nat such that

           A12: (s " ) < n by SEQ_4: 3;

          assume 0 < s;

          then

           A13: 0 < (s " );

          ((s " ) + 0 ) < (n + 1) by A12, XREAL_1: 8;

          then (1 / (n + 1)) < (1 / (s " )) by A13, XREAL_1: 76;

          then

           A14: (1 / (n + 1)) < s by XCMPLX_1: 216;

          take k = n;

          let m be Nat;

          

           A15: m in NAT by ORDINAL1:def 12;

          assume k <= m;

          then (k + 1) <= (m + 1) by XREAL_1: 6;

          then (1 / (m + 1)) <= (1 / (k + 1)) by XREAL_1: 118;

          then (1 / (m + 1)) < s by A14, XXREAL_0: 2;

          hence ||.((s1 . m) - x0).|| < s by A6, XXREAL_0: 2, A15;

        end;

        then

         A16: s1 is convergent by NORMSP_1:def 6;

        then ( lim s1) = x0 by A11, NORMSP_1:def 7;

        then (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1)) by A1, A7, A16;

        then

        consider n be Nat such that

         A17: for m be Nat st n <= m holds ||.(((f /* s1) . m) - (f /. x0)).|| < r by A2, NORMSP_1:def 7;

         ||.(((f /* s1) . n) - (f /. x0)).|| < r by A17;

        hence contradiction by A9;

      end;

      assume that

       A18: x0 in ( dom f) and

       A19: 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;

      now

        let s1 such that

         A20: ( rng s1) c= ( dom f) and

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

         A22:

        now

          let p be Real;

          assume 0 < p;

          then

          consider s such that

           A23: 0 < s and

           A24: for x1 st x1 in ( dom f) & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < p by A19;

          reconsider s as Real;

          consider n be Nat such that

           A25: for m be Nat st n <= m holds ||.((s1 . m) - x0).|| < s by A21, A23, NORMSP_1:def 7;

          take k = n;

          let m be Nat;

          assume k <= m;

          then

           A26: ||.((s1 . m) - x0).|| < s by A25;

          

           A27: m in NAT by ORDINAL1:def 12;

          ( dom s1) = NAT by FUNCT_2:def 1;

          then (s1 . m) in ( rng s1) by FUNCT_1: 3, A27;

          then ||.((f /. (s1 . m)) - (f /. x0)).|| < p by A20, A24, A26;

          hence ||.(((f /* s1) . m) - (f /. x0)).|| < p by A20, FUNCT_2: 109, A27;

        end;

        then (f /* s1) is convergent by NORMSP_1:def 6;

        hence (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1)) by A22, NORMSP_1:def 7;

      end;

      hence thesis by A18;

    end;

    theorem :: NFCONT_1:8

    

     Th8: for f be PartFunc of the carrier of S, REAL holds (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

      let f be PartFunc of the carrier of S, REAL ;

      thus f is_continuous_in x0 implies 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

        assume

         A1: f is_continuous_in x0;

        hence x0 in ( dom f);

        given r such that

         A2: 0 < r and

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

        defpred P[ Nat, Point of S] means $2 in ( dom f) & ||.($2 - x0).|| < (1 / ($1 + 1)) & not |.((f /. $2) - (f /. x0)).| < r;

        

         A4: for n be Element of NAT holds ex p be Point of S st P[n, p]

        proof

          let n be Element of NAT ;

           0 < ((n + 1) " );

          then 0 < (1 / (n + 1)) by XCMPLX_1: 215;

          then

          consider p be Point of S such that

           A5: p in ( dom f) & ||.(p - x0).|| < (1 / (n + 1)) & |.((f /. p) - (f /. x0)).| >= r by A3;

          take p;

          thus thesis by A5;

        end;

        consider s1 be sequence of S such that

         A6: for n be Element of NAT holds P[n, (s1 . n)] from FUNCT_2:sch 3( A4);

        reconsider s1 as sequence of S;

        

         A7: ( rng s1) c= ( dom f)

        proof

          

           A8: ( dom s1) = NAT by FUNCT_2:def 1;

          let v be object;

          assume v in ( rng s1);

          then ex n be object st n in NAT & v = (s1 . n) by A8, FUNCT_1:def 3;

          hence thesis by A6;

        end;

         A9:

        now

          let n;

          

           A10: n in NAT by ORDINAL1:def 12;

           |.((f /. (s1 . n)) - (f /. x0)).| >= r by A6, A10;

          hence |.(((f /* s1) . n) - (f /. x0)).| >= r by A7, FUNCT_2: 109, A10;

        end;

         A11:

        now

          let s be Real;

          consider n be Nat such that

           A12: (s " ) < n by SEQ_4: 3;

          assume 0 < s;

          then

           A13: 0 < (s " );

          ((s " ) + 0 ) < (n + 1) by A12, XREAL_1: 8;

          then (1 / (n + 1)) < (1 / (s " )) by A13, XREAL_1: 76;

          then

           A14: (1 / (n + 1)) < s by XCMPLX_1: 216;

          take k = n;

          let m be Nat;

          

           A15: m in NAT by ORDINAL1:def 12;

          assume k <= m;

          then (k + 1) <= (m + 1) by XREAL_1: 6;

          then (1 / (m + 1)) <= (1 / (k + 1)) by XREAL_1: 118;

          then (1 / (m + 1)) < s by A14, XXREAL_0: 2;

          hence ||.((s1 . m) - x0).|| < s by A6, XXREAL_0: 2, A15;

        end;

        then

         A16: s1 is convergent by NORMSP_1:def 6;

        then ( lim s1) = x0 by A11, NORMSP_1:def 7;

        then (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1)) by A1, A7, A16;

        then

        consider n be Nat such that

         A17: for m be Nat st n <= m holds |.(((f /* s1) . m) - (f /. x0)).| < r by A2, SEQ_2:def 7;

         |.(((f /* s1) . n) - (f /. x0)).| < r by A17;

        hence contradiction by A9;

      end;

      assume that

       A18: x0 in ( dom f) and

       A19: 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;

      now

        let s1 such that

         A20: ( rng s1) c= ( dom f) and

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

         A22:

        now

          let p be Real;

          reconsider pp = p as Real;

          assume 0 < p;

          then

          consider s such that

           A23: 0 < s and

           A24: for x1 st x1 in ( dom f) & ||.(x1 - x0).|| < s holds |.((f /. x1) - (f /. x0)).| < pp by A19;

          reconsider s as Real;

          consider n be Nat such that

           A25: for m be Nat st n <= m holds ||.((s1 . m) - x0).|| < s by A21, A23, NORMSP_1:def 7;

          take k = n;

          let m be Nat;

          

           A26: m in NAT by ORDINAL1:def 12;

          assume k <= m;

          then

           A27: ||.((s1 . m) - x0).|| < s by A25;

          ( dom s1) = NAT by FUNCT_2:def 1;

          then (s1 . m) in ( rng s1) by FUNCT_1: 3, A26;

          then |.((f /. (s1 . m)) - (f /. x0)).| < p by A20, A24, A27;

          hence |.(((f /* s1) . m) - (f /. x0)).| < p by A20, FUNCT_2: 109, A26;

        end;

        then (f /* s1) is convergent by SEQ_2:def 6;

        hence (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1)) by A22, SEQ_2:def 7;

      end;

      hence thesis by A18;

    end;

    theorem :: NFCONT_1:9

    

     Th9: for f, x0 holds f is_continuous_in x0 iff x0 in ( dom f) & for N1 be Neighbourhood of (f /. x0) holds ex N be Neighbourhood of x0 st for x1 st x1 in ( dom f) & x1 in N holds (f /. x1) in N1

    proof

      let f, x0;

      thus f is_continuous_in x0 implies x0 in ( dom f) & for N1 be Neighbourhood of (f /. x0) 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

         A1: f is_continuous_in x0;

        hence x0 in ( dom f);

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

        consider r such that

         A2: 0 < r and

         A3: { y where y be Point of T : ||.(y - (f /. x0)).|| < r } c= N1 by Def1;

        consider s such that

         A4: 0 < s and

         A5: for x1 st x1 in ( dom f) & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r by A1, A2, Th7;

        reconsider s as Real;

        reconsider N = { z where z be Point of S : ||.(z - x0).|| < s } as Neighbourhood of x0 by A4, Th3;

        take N;

        let x1;

        assume that

         A6: x1 in ( dom f) and

         A7: x1 in N;

        ex z be Point of S st x1 = z & ||.(z - x0).|| < s by A7;

        then ||.((f /. x1) - (f /. x0)).|| < r by A5, A6;

        then (f /. x1) in { y where y be Point of T : ||.(y - (f /. x0)).|| < r };

        hence thesis by A3;

      end;

      assume that

       A8: x0 in ( dom f) and

       A9: for N1 be Neighbourhood of (f /. x0) holds ex N be Neighbourhood of x0 st for x1 st x1 in ( dom f) & x1 in N holds (f /. x1) in N1;

      now

        let r;

        assume

         A10: 0 < r;

        reconsider rr = r as Real;

        reconsider N1 = { y where y be Point of T : ||.(y - (f /. x0)).|| < rr } as Neighbourhood of (f /. x0) by Th3, A10;

        consider N2 be Neighbourhood of x0 such that

         A11: for x1 st x1 in ( dom f) & x1 in N2 holds (f /. x1) in N1 by A9;

        consider s such that

         A12: 0 < s and

         A13: { z where z be Point of S : ||.(z - x0).|| < s } c= N2 by Def1;

        take s;

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

        proof

          let x1;

          assume that

           A14: x1 in ( dom f) and

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

          x1 in { z where z be Point of S : ||.(z - x0).|| < s } by A15;

          then (f /. x1) in N1 by A11, A13, A14;

          then ex y be Point of T st (f /. x1) = y & ||.(y - (f /. x0)).|| < r;

          hence thesis;

        end;

        hence 0 < s & for x1 st x1 in ( dom f) & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r by A12;

      end;

      hence thesis by A8, Th7;

    end;

    theorem :: NFCONT_1:10

    

     Th10: for f, x0 holds f is_continuous_in x0 iff x0 in ( dom f) & for N1 be Neighbourhood of (f /. x0) holds ex N be Neighbourhood of x0 st (f .: N) c= N1

    proof

      let f, x0;

      thus f is_continuous_in x0 implies x0 in ( dom f) & for N1 be Neighbourhood of (f /. x0) holds ex N be Neighbourhood of x0 st (f .: N) c= N1

      proof

        assume

         A1: f is_continuous_in x0;

        hence x0 in ( dom f);

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

        consider N be Neighbourhood of x0 such that

         A2: for x1 st x1 in ( dom f) & x1 in N holds (f /. x1) in N1 by A1, Th9;

        take N;

        now

          let r be object;

          assume r in (f .: N);

          then

          consider x be Point of S such that

           A3: x in ( dom f) and

           A4: x in N and

           A5: r = (f . x) by PARTFUN2: 59;

          r = (f /. x) by A3, A5, PARTFUN1:def 6;

          hence r in N1 by A2, A3, A4;

        end;

        hence thesis;

      end;

      assume that

       A6: x0 in ( dom f) and

       A7: for N1 be Neighbourhood of (f /. x0) holds ex N be Neighbourhood of x0 st (f .: N) c= N1;

      now

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

        consider N be Neighbourhood of x0 such that

         A8: (f .: N) c= N1 by A7;

        take N;

        let x1;

        assume that

         A9: x1 in ( dom f) and

         A10: x1 in N;

        (f . x1) in (f .: N) by A9, A10, FUNCT_1:def 6;

        then (f . x1) in N1 by A8;

        hence (f /. x1) in N1 by A9, PARTFUN1:def 6;

      end;

      hence thesis by A6, Th9;

    end;

    theorem :: NFCONT_1:11

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

    proof

      assume

       A1: x0 in ( dom f);

      given N be Neighbourhood of x0 such that

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

      now

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

        take N;

        

         A3: (f /. x0) in N1 by Th4;

        (f .: N) = ( Im (f,x0)) by A2, RELAT_1: 112

        .= {(f . x0)} by A1, FUNCT_1: 59

        .= {(f /. x0)} by A1, PARTFUN1:def 6;

        hence (f .: N) c= N1 by A3, ZFMISC_1: 31;

      end;

      hence thesis by A1, Th10;

    end;

    theorem :: NFCONT_1:12

    

     Th12: for h1,h2 be PartFunc of S, T holds for seq be sequence of S st ( rng seq) c= (( dom h1) /\ ( dom h2)) holds ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) & ((h1 - h2) /* seq) = ((h1 /* seq) - (h2 /* seq))

    proof

      let h1,h2 be PartFunc of S, T;

      let seq be sequence of S;

      

       A1: (( dom h1) /\ ( dom h2)) c= ( dom h1) by XBOOLE_1: 17;

      

       A2: (( dom h1) /\ ( dom h2)) c= ( dom h2) by XBOOLE_1: 17;

      assume

       A3: ( rng seq) c= (( dom h1) /\ ( dom h2));

      then

       A4: ( rng seq) c= ( dom (h1 + h2)) by VFUNCT_1:def 1;

      now

        let n be Nat;

        

         A5: n in NAT by ORDINAL1:def 12;

        

         A6: (seq . n) in ( dom (h1 + h2)) by A4, Th5;

        

        thus (((h1 + h2) /* seq) . n) = ((h1 + h2) /. (seq . n)) by A4, FUNCT_2: 109, A5

        .= ((h1 /. (seq . n)) + (h2 /. (seq . n))) by A6, VFUNCT_1:def 1

        .= (((h1 /* seq) . n) + (h2 /. (seq . n))) by A3, A1, FUNCT_2: 109, XBOOLE_1: 1, A5

        .= (((h1 /* seq) . n) + ((h2 /* seq) . n)) by A3, A2, FUNCT_2: 109, XBOOLE_1: 1, A5;

      end;

      hence ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) by NORMSP_1:def 2;

      

       A7: ( rng seq) c= ( dom (h1 - h2)) by A3, VFUNCT_1:def 2;

      now

        let n be Nat;

        

         A8: n in NAT by ORDINAL1:def 12;

        

         A9: (seq . n) in ( dom (h1 - h2)) by A7, Th5;

        

        thus (((h1 - h2) /* seq) . n) = ((h1 - h2) /. (seq . n)) by A7, FUNCT_2: 109, A8

        .= ((h1 /. (seq . n)) - (h2 /. (seq . n))) by A9, VFUNCT_1:def 2

        .= (((h1 /* seq) . n) - (h2 /. (seq . n))) by A3, A1, FUNCT_2: 109, XBOOLE_1: 1, A8

        .= (((h1 /* seq) . n) - ((h2 /* seq) . n)) by A3, A2, FUNCT_2: 109, XBOOLE_1: 1, A8;

      end;

      hence thesis by NORMSP_1:def 3;

    end;

    theorem :: NFCONT_1:13

    

     Th13: for h be PartFunc of S, T holds for seq be sequence of S holds for r be Real st ( rng seq) c= ( dom h) holds ((r (#) h) /* seq) = (r * (h /* seq))

    proof

      let h be PartFunc of S, T;

      let seq be sequence of S;

      let r be Real;

      assume

       A1: ( rng seq) c= ( dom h);

      then

       A2: ( rng seq) c= ( dom (r (#) h)) by VFUNCT_1:def 4;

      now

        let n be Nat;

        

         A3: n in NAT by ORDINAL1:def 12;

        

         A4: (seq . n) in ( dom (r (#) h)) by A2, Th5;

        

        thus (((r (#) h) /* seq) . n) = ((r (#) h) /. (seq . n)) by A2, FUNCT_2: 109, A3

        .= (r * (h /. (seq . n))) by A4, VFUNCT_1:def 4

        .= (r * ((h /* seq) . n)) by A1, FUNCT_2: 109, A3;

      end;

      hence thesis by NORMSP_1:def 5;

    end;

    reconsider jj = 1 as Real;

    theorem :: NFCONT_1:14

    

     Th14: for h be PartFunc of S, T holds for seq be sequence of S st ( rng seq) c= ( dom h) holds ||.(h /* seq).|| = ( ||.h.|| /* seq) & ( - (h /* seq)) = (( - h) /* seq)

    proof

      let h be PartFunc of S, T;

      let seq be sequence of S;

      assume

       A1: ( rng seq) c= ( dom h);

      then

       A2: ( rng seq) c= ( dom ||.h.||) by NORMSP_0:def 3;

      now

        let n be Element of NAT ;

        (seq . n) in ( rng seq) by Th6;

        then (seq . n) in ( dom h) by A1;

        then

         A3: (seq . n) in ( dom ||.h.||) by NORMSP_0:def 3;

        

        thus ( ||.(h /* seq).|| . n) = ||.((h /* seq) . n).|| by NORMSP_0:def 4

        .= ||.(h /. (seq . n)).|| by A1, FUNCT_2: 109

        .= ( ||.h.|| . (seq . n)) by A3, NORMSP_0:def 3

        .= ( ||.h.|| /. (seq . n)) by A3, PARTFUN1:def 6

        .= (( ||.h.|| /* seq) . n) by A2, FUNCT_2: 109;

      end;

      hence ||.(h /* seq).|| = ( ||.h.|| /* seq) by FUNCT_2: 63;

      

      thus ( - (h /* seq)) = (( - jj) * (h /* seq)) by Th2

      .= ((( - 1) (#) h) /* seq) by A1, Th13

      .= (( - h) /* seq) by VFUNCT_1: 23;

    end;

    theorem :: NFCONT_1:15

    f1 is_continuous_in x0 & f2 is_continuous_in x0 implies (f1 + f2) is_continuous_in x0 & (f1 - f2) is_continuous_in x0

    proof

      assume that

       A1: f1 is_continuous_in x0 and

       A2: f2 is_continuous_in x0;

      

       A3: x0 in ( dom f1) & x0 in ( dom f2) by A1, A2;

      now

        x0 in (( dom f1) /\ ( dom f2)) by A3, XBOOLE_0:def 4;

        hence

         A4: x0 in ( dom (f1 + f2)) by VFUNCT_1:def 1;

        let s1;

        assume that

         A5: ( rng s1) c= ( dom (f1 + f2)) and

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

        

         A7: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A5, VFUNCT_1:def 1;

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

        then ( dom (f1 + f2)) c= ( dom f2) by XBOOLE_1: 17;

        then

         A8: ( rng s1) c= ( dom f2) by A5;

        then

         A9: (f2 /* s1) is convergent by A2, A6;

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

        then ( dom (f1 + f2)) c= ( dom f1) by XBOOLE_1: 17;

        then

         A10: ( rng s1) c= ( dom f1) by A5;

        then

         A11: (f1 /* s1) is convergent by A1, A6;

        then ((f1 /* s1) + (f2 /* s1)) is convergent by A9, NORMSP_1: 19;

        hence ((f1 + f2) /* s1) is convergent by A7, Th12;

        

         A12: (f1 /. x0) = ( lim (f1 /* s1)) by A1, A6, A10;

        

         A13: (f2 /. x0) = ( lim (f2 /* s1)) by A2, A6, A8;

        

        thus ((f1 + f2) /. x0) = ((f1 /. x0) + (f2 /. x0)) by A4, VFUNCT_1:def 1

        .= ( lim ((f1 /* s1) + (f2 /* s1))) by A11, A12, A9, A13, NORMSP_1: 25

        .= ( lim ((f1 + f2) /* s1)) by A7, Th12;

      end;

      hence (f1 + f2) is_continuous_in x0;

      now

        x0 in (( dom f1) /\ ( dom f2)) by A3, XBOOLE_0:def 4;

        hence

         A14: x0 in ( dom (f1 - f2)) by VFUNCT_1:def 2;

        let s1;

        assume that

         A15: ( rng s1) c= ( dom (f1 - f2)) and

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

        

         A17: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A15, VFUNCT_1:def 2;

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

        then ( dom (f1 - f2)) c= ( dom f2) by XBOOLE_1: 17;

        then

         A18: ( rng s1) c= ( dom f2) by A15;

        then

         A19: (f2 /* s1) is convergent by A2, A16;

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

        then ( dom (f1 - f2)) c= ( dom f1) by XBOOLE_1: 17;

        then

         A20: ( rng s1) c= ( dom f1) by A15;

        then

         A21: (f1 /* s1) is convergent by A1, A16;

        then ((f1 /* s1) - (f2 /* s1)) is convergent by A19, NORMSP_1: 20;

        hence ((f1 - f2) /* s1) is convergent by A17, Th12;

        

         A22: (f1 /. x0) = ( lim (f1 /* s1)) by A1, A16, A20;

        

         A23: (f2 /. x0) = ( lim (f2 /* s1)) by A2, A16, A18;

        

        thus ((f1 - f2) /. x0) = ((f1 /. x0) - (f2 /. x0)) by A14, VFUNCT_1:def 2

        .= ( lim ((f1 /* s1) - (f2 /* s1))) by A21, A22, A19, A23, NORMSP_1: 26

        .= ( lim ((f1 - f2) /* s1)) by A17, Th12;

      end;

      hence thesis;

    end;

    theorem :: NFCONT_1:16

    

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

    proof

      assume

       A1: f is_continuous_in x0;

      then x0 in ( dom f);

      hence

       A2: x0 in ( dom (r (#) f)) by VFUNCT_1:def 4;

      let s1;

      assume that

       A3: ( rng s1) c= ( dom (r (#) f)) and

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

      

       A5: ( rng s1) c= ( dom f) by A3, VFUNCT_1:def 4;

      then

       A6: (f /. x0) = ( lim (f /* s1)) by A1, A4;

      reconsider rr = r as Real;

      

       A7: (f /* s1) is convergent by A1, A4, A5;

      then (r * (f /* s1)) is convergent by NORMSP_1: 22;

      hence ((r (#) f) /* s1) is convergent by A5, Th13;

      

      thus ((r (#) f) /. x0) = (r * (f /. x0)) by A2, VFUNCT_1:def 4

      .= ( lim (r * (f /* s1))) by A7, A6, NORMSP_1: 28

      .= ( lim ((r (#) f) /* s1)) by A5, Th13;

    end;

    theorem :: NFCONT_1:17

    f is_continuous_in x0 implies ||.f.|| is_continuous_in x0 & ( - f) is_continuous_in x0

    proof

      assume

       A1: f is_continuous_in x0;

      then

       A2: x0 in ( dom f);

      now

        thus

         A3: x0 in ( dom ||.f.||) by A2, NORMSP_0:def 3;

        let s1;

        assume that

         A4: ( rng s1) c= ( dom ||.f.||) and

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

        

         A6: ( rng s1) c= ( dom f) by A4, NORMSP_0:def 3;

        then

         A7: (f /. x0) = ( lim (f /* s1)) by A1, A5;

        

         A8: (f /* s1) is convergent by A1, A5, A6;

        then ||.(f /* s1).|| is convergent by NORMSP_1: 23;

        hence ( ||.f.|| /* s1) is convergent by A6, Th14;

        

        thus ( ||.f.|| /. x0) = ( ||.f.|| . x0) by A3, PARTFUN1:def 6

        .= ||.(f /. x0).|| by A3, NORMSP_0:def 3

        .= ( lim ||.(f /* s1).||) by A8, A7, LOPBAN_1: 41

        .= ( lim ( ||.f.|| /* s1)) by A6, Th14;

      end;

      hence ||.f.|| is_continuous_in x0;

      ( - f) = (( - 1) (#) f) by VFUNCT_1: 23;

      hence thesis by A1, Th16;

    end;

    definition

      let S, T;

      let f, X;

      :: NFCONT_1:def7

      pred f is_continuous_on X means X c= ( dom f) & for x0 st x0 in X holds (f | X) is_continuous_in x0;

    end

    definition

      let S;

      let f be PartFunc of the carrier of S, REAL ;

      let X;

      :: NFCONT_1:def8

      pred f is_continuous_on X means X c= ( dom f) & for x0 st x0 in X holds (f | X) is_continuous_in x0;

    end

    theorem :: NFCONT_1:18

    

     Th18: for X, f holds f is_continuous_on X iff X c= ( dom f) & for s1 st ( rng s1) c= X & s1 is convergent & ( lim s1) in X holds (f /* s1) is convergent & (f /. ( lim s1)) = ( lim (f /* s1))

    proof

      let X, f;

      thus f is_continuous_on X implies X c= ( dom f) & for s1 st ( rng s1) c= X & s1 is convergent & ( lim s1) in X holds (f /* s1) is convergent & (f /. ( lim s1)) = ( lim (f /* s1))

      proof

        assume

         A1: f is_continuous_on X;

        then

         A2: X c= ( dom f);

        now

          let s1 such that

           A3: ( rng s1) c= X and

           A4: s1 is convergent and

           A5: ( lim s1) in X;

          

           A6: (f | X) is_continuous_in ( lim s1) by A1, A5;

          

           A7: ( dom (f | X)) = (( dom f) /\ X) by PARTFUN2: 15

          .= X by A2, XBOOLE_1: 28;

          now

            let n be Element of NAT ;

            ( dom s1) = NAT by FUNCT_2:def 1;

            then

             A8: (s1 . n) in ( rng s1) by FUNCT_1: 3;

            

            thus (((f | X) /* s1) . n) = ((f | X) /. (s1 . n)) by A3, A7, FUNCT_2: 109

            .= (f /. (s1 . n)) by A3, A7, A8, PARTFUN2: 15

            .= ((f /* s1) . n) by A2, A3, FUNCT_2: 109, XBOOLE_1: 1;

          end;

          then

           A9: ((f | X) /* s1) = (f /* s1) by FUNCT_2: 63;

          (f /. ( lim s1)) = ((f | X) /. ( lim s1)) by A5, A7, PARTFUN2: 15

          .= ( lim (f /* s1)) by A3, A4, A7, A6, A9;

          hence (f /* s1) is convergent & (f /. ( lim s1)) = ( lim (f /* s1)) by A3, A4, A7, A6, A9;

        end;

        hence thesis by A1;

      end;

      assume that

       A10: X c= ( dom f) and

       A11: for s1 st ( rng s1) c= X & s1 is convergent & ( lim s1) in X holds (f /* s1) is convergent & (f /. ( lim s1)) = ( lim (f /* s1));

      now

        

         A12: ( dom (f | X)) = (( dom f) /\ X) by PARTFUN2: 15

        .= X by A10, XBOOLE_1: 28;

        let x1 such that

         A13: x1 in X;

        now

          let s1 such that

           A14: ( rng s1) c= ( dom (f | X)) and

           A15: s1 is convergent and

           A16: ( lim s1) = x1;

          now

            let n be Element of NAT ;

            ( dom s1) = NAT by FUNCT_2:def 1;

            then

             A17: (s1 . n) in ( rng s1) by FUNCT_1: 3;

            

            thus (((f | X) /* s1) . n) = ((f | X) /. (s1 . n)) by A14, FUNCT_2: 109

            .= (f /. (s1 . n)) by A14, A17, PARTFUN2: 15

            .= ((f /* s1) . n) by A10, A12, A14, FUNCT_2: 109, XBOOLE_1: 1;

          end;

          then

           A18: ((f | X) /* s1) = (f /* s1) by FUNCT_2: 63;

          ((f | X) /. ( lim s1)) = (f /. ( lim s1)) by A13, A12, A16, PARTFUN2: 15

          .= ( lim ((f | X) /* s1)) by A11, A13, A12, A14, A15, A16, A18;

          hence ((f | X) /* s1) is convergent & ((f | X) /. x1) = ( lim ((f | X) /* s1)) by A11, A13, A12, A14, A15, A16, A18;

        end;

        hence (f | X) is_continuous_in x1 by A13, A12;

      end;

      hence thesis by A10;

    end;

    theorem :: NFCONT_1:19

    

     Th19: f is_continuous_on X iff X c= ( dom f) & 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

      thus f is_continuous_on X implies X c= ( dom f) & 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: f is_continuous_on X;

        hence X c= ( dom f);

        

         A2: X c= ( dom f) by A1;

        let x0, r;

        assume that

         A3: x0 in X and

         A4: 0 < r;

        (f | X) is_continuous_in x0 by A1, A3;

        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, Th7;

        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 PARTFUN2: 15

        .= X by A2, 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 that

       A10: X c= ( dom f) and

       A11: 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;

      

       A12: ( dom (f | X)) = (( dom f) /\ X) by PARTFUN2: 15

      .= X by A10, XBOOLE_1: 28;

      now

        let x0 such that

         A13: x0 in X;

        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 A11, 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, A13, PARTFUN2: 15

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

          hence thesis by A12, A15, A16, A17;

        end;

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

      end;

      hence thesis by A10;

    end;

    theorem :: NFCONT_1:20

    for f be PartFunc of the carrier of S, REAL holds (f is_continuous_on X iff X c= ( dom f) & 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

      let f be PartFunc of the carrier of S, REAL ;

      thus f is_continuous_on X implies X c= ( dom f) & 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: f is_continuous_on X;

        hence X c= ( dom f);

        

         A2: X c= ( dom f) by A1;

        let x0, r;

        assume that

         A3: x0 in X and

         A4: 0 < r;

        (f | X) is_continuous_in x0 by A1, A3;

        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, Th8;

        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 PARTFUN2: 15

        .= X by A2, 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 that

       A10: X c= ( dom f) and

       A11: 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;

      

       A12: ( dom (f | X)) = (( dom f) /\ X) by PARTFUN2: 15

      .= X by A10, XBOOLE_1: 28;

      now

        let x0 such that

         A13: x0 in X;

        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 A11, 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, A13, PARTFUN2: 15

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

          hence thesis by A12, A15, A16, A17;

        end;

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

      end;

      hence thesis by A10;

    end;

    theorem :: NFCONT_1:21

    f is_continuous_on X iff (f | X) is_continuous_on X

    proof

      thus f is_continuous_on X implies (f | X) is_continuous_on X

      proof

        assume

         A1: f is_continuous_on X;

        then X c= ( dom f);

        then X c= (( dom f) /\ X) by XBOOLE_1: 28;

        hence X c= ( dom (f | X)) by RELAT_1: 61;

        let r be Point of S;

        assume r in X;

        then (f | X) is_continuous_in r by A1;

        hence thesis by RELAT_1: 72;

      end;

      assume

       A2: (f | X) is_continuous_on X;

      then X c= ( dom (f | X));

      then (( dom f) /\ X) c= ( dom f) & X c= (( dom f) /\ X) by RELAT_1: 61, XBOOLE_1: 17;

      hence X c= ( dom f);

      let r be Point of S;

      assume r in X;

      then ((f | X) | X) is_continuous_in r by A2;

      hence thesis by RELAT_1: 72;

    end;

    theorem :: NFCONT_1:22

    

     Th22: for f be PartFunc of the carrier of S, REAL holds (f is_continuous_on X iff (f | X) is_continuous_on X)

    proof

      let f be PartFunc of the carrier of S, REAL ;

      thus f is_continuous_on X implies (f | X) is_continuous_on X

      proof

        assume

         A1: f is_continuous_on X;

        then X c= ( dom f);

        then X c= (( dom f) /\ X) by XBOOLE_1: 28;

        hence X c= ( dom (f | X)) by RELAT_1: 61;

        let r be Point of S;

        assume r in X;

        then (f | X) is_continuous_in r by A1;

        hence thesis by RELAT_1: 72;

      end;

      assume

       A2: (f | X) is_continuous_on X;

      then X c= ( dom (f | X));

      then (( dom f) /\ X) c= ( dom f) & X c= (( dom f) /\ X) by RELAT_1: 61, XBOOLE_1: 17;

      hence X c= ( dom f);

      let r be Point of S;

      assume r in X;

      then ((f | X) | X) is_continuous_in r by A2;

      hence thesis by RELAT_1: 72;

    end;

    theorem :: NFCONT_1:23

    

     Th23: f is_continuous_on X & X1 c= X implies f is_continuous_on X1

    proof

      assume that

       A1: f is_continuous_on X and

       A2: X1 c= X;

      X c= ( dom f) by A1;

      hence

       A3: X1 c= ( dom f) by A2;

      let r be Point of S;

      assume

       A4: r in X1;

      then

       A5: (f | X) is_continuous_in r by A1, A2;

      thus (f | X1) is_continuous_in r

      proof

        (( dom f) /\ X1) c= (( dom f) /\ X) by A2, XBOOLE_1: 26;

        then ( dom (f | X1)) c= (( dom f) /\ X) by RELAT_1: 61;

        then

         A6: ( dom (f | X1)) c= ( dom (f | X)) by RELAT_1: 61;

        r in (( dom f) /\ X1) by A3, A4, XBOOLE_0:def 4;

        hence

         A7: r in ( dom (f | X1)) by RELAT_1: 61;

        

        then

         A8: ((f | X) /. r) = (f /. r) by A6, PARTFUN2: 15

        .= ((f | X1) /. r) by A7, PARTFUN2: 15;

        let s1 such that

         A9: ( rng s1) c= ( dom (f | X1)) and

         A10: s1 is convergent & ( lim s1) = r;

        

         A11: ( rng s1) c= ( dom (f | X)) by A9, A6;

         A12:

        now

          let n be Element of NAT ;

          ( dom s1) = NAT by FUNCT_2:def 1;

          then

           A13: (s1 . n) in ( rng s1) by FUNCT_1: 3;

          

          thus (((f | X) /* s1) . n) = ((f | X) /. (s1 . n)) by A9, A6, FUNCT_2: 109, XBOOLE_1: 1

          .= (f /. (s1 . n)) by A11, A13, PARTFUN2: 15

          .= ((f | X1) /. (s1 . n)) by A9, A13, PARTFUN2: 15

          .= (((f | X1) /* s1) . n) by A9, FUNCT_2: 109;

        end;

        ((f | X) /* s1) is convergent & ((f | X) /. r) = ( lim ((f | X) /* s1)) by A5, A10, A11;

        hence thesis by A8, A12, FUNCT_2: 63;

      end;

    end;

    theorem :: NFCONT_1:24

    x0 in ( dom f) implies f is_continuous_on {x0}

    proof

      assume

       A1: x0 in ( dom f);

      thus {x0} c= ( dom f) by A1, TARSKI:def 1;

      let p be Point of S such that

       A2: p in {x0};

      thus (f | {x0}) is_continuous_in p

      proof

        p in ( dom f) by A1, A2, TARSKI:def 1;

        then p in (( dom f) /\ {x0}) by A2, XBOOLE_0:def 4;

        hence p in ( dom (f | {x0})) by RELAT_1: 61;

        let s1;

        assume that

         A3: ( rng s1) c= ( dom (f | {x0})) and s1 is convergent and ( lim s1) = p;

        

         A4: (( dom f) /\ {x0}) c= {x0} by XBOOLE_1: 17;

        ( rng s1) c= (( dom f) /\ {x0}) by A3, RELAT_1: 61;

        then

         A5: ( rng s1) c= {x0} by A4;

         A6:

        now

          let n;

          

           A7: n in NAT by ORDINAL1:def 12;

          ( dom s1) = NAT by FUNCT_2:def 1;

          then (s1 . n) in ( rng s1) by FUNCT_1: 3, A7;

          hence (s1 . n) = x0 by A5, TARSKI:def 1;

        end;

        

         A8: p = x0 by A2, TARSKI:def 1;

         A9:

        now

          let g be Real such that

           A10: 0 < g;

          reconsider n = 0 as Nat;

          take n;

          let m be Nat such that n <= m;

          

           A11: m in NAT by ORDINAL1:def 12;

           ||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| = ||.(((f | {x0}) /. (s1 . m)) - ((f | {x0}) /. x0)).|| by A8, A3, FUNCT_2: 109, A11

          .= ||.(((f | {x0}) /. x0) - ((f | {x0}) /. x0)).|| by A6

          .= ||.( 0. T).|| by RLVECT_1: 15

          .= 0 by NORMSP_1: 1;

          hence ||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g by A10;

        end;

        hence ((f | {x0}) /* s1) is convergent by NORMSP_1:def 6;

        hence thesis by A9, NORMSP_1:def 7;

      end;

    end;

    theorem :: NFCONT_1:25

    

     Th25: for X, f1, f2 st f1 is_continuous_on X & f2 is_continuous_on X holds (f1 + f2) is_continuous_on X & (f1 - f2) is_continuous_on X

    proof

      let X, f1, f2;

      assume

       A1: f1 is_continuous_on X & f2 is_continuous_on X;

      then X c= ( dom f1) & X c= ( dom f2);

      then

       A2: X c= (( dom f1) /\ ( dom f2)) by XBOOLE_1: 19;

      then

       A3: X c= ( dom (f1 + f2)) by VFUNCT_1:def 1;

      now

        let s1;

        assume that

         A4: ( rng s1) c= X and

         A5: s1 is convergent and

         A6: ( lim s1) in X;

        

         A7: (f1 /* s1) is convergent & (f2 /* s1) is convergent by A1, A4, A5, A6, Th18;

        then

         A8: ((f1 /* s1) + (f2 /* s1)) is convergent by NORMSP_1: 19;

        

         A9: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A2, A4;

        (f1 /. ( lim s1)) = ( lim (f1 /* s1)) & (f2 /. ( lim s1)) = ( lim (f2 /* s1)) by A1, A4, A5, A6, Th18;

        

        then ((f1 + f2) /. ( lim s1)) = (( lim (f1 /* s1)) + ( lim (f2 /* s1))) by A3, A6, VFUNCT_1:def 1

        .= ( lim ((f1 /* s1) + (f2 /* s1))) by A7, NORMSP_1: 25

        .= ( lim ((f1 + f2) /* s1)) by A9, Th12;

        hence ((f1 + f2) /* s1) is convergent & ((f1 + f2) /. ( lim s1)) = ( lim ((f1 + f2) /* s1)) by A9, A8, Th12;

      end;

      hence (f1 + f2) is_continuous_on X by A3, Th18;

      

       A10: X c= ( dom (f1 - f2)) by A2, VFUNCT_1:def 2;

      now

        let s1;

        assume that

         A11: ( rng s1) c= X and

         A12: s1 is convergent and

         A13: ( lim s1) in X;

        

         A14: (f1 /* s1) is convergent & (f2 /* s1) is convergent by A1, A11, A12, A13, Th18;

        then

         A15: ((f1 /* s1) - (f2 /* s1)) is convergent by NORMSP_1: 20;

        

         A16: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A2, A11;

        (f1 /. ( lim s1)) = ( lim (f1 /* s1)) & (f2 /. ( lim s1)) = ( lim (f2 /* s1)) by A1, A11, A12, A13, Th18;

        

        then ((f1 - f2) /. ( lim s1)) = (( lim (f1 /* s1)) - ( lim (f2 /* s1))) by A10, A13, VFUNCT_1:def 2

        .= ( lim ((f1 /* s1) - (f2 /* s1))) by A14, NORMSP_1: 26

        .= ( lim ((f1 - f2) /* s1)) by A16, Th12;

        hence ((f1 - f2) /* s1) is convergent & ((f1 - f2) /. ( lim s1)) = ( lim ((f1 - f2) /* s1)) by A16, A15, Th12;

      end;

      hence thesis by A10, Th18;

    end;

    theorem :: NFCONT_1:26

    for X, X1, f1, f2 st f1 is_continuous_on X & f2 is_continuous_on X1 holds (f1 + f2) is_continuous_on (X /\ X1) & (f1 - f2) is_continuous_on (X /\ X1)

    proof

      let X, X1, f1, f2;

      assume f1 is_continuous_on X & f2 is_continuous_on X1;

      then f1 is_continuous_on (X /\ X1) & f2 is_continuous_on (X /\ X1) by Th23, XBOOLE_1: 17;

      hence thesis by Th25;

    end;

    theorem :: NFCONT_1:27

    

     Th27: for r, X, f st f is_continuous_on X holds (r (#) f) is_continuous_on X

    proof

      let r, X, f;

      assume

       A1: f is_continuous_on X;

      then

       A2: X c= ( dom f);

      then

       A3: X c= ( dom (r (#) f)) by VFUNCT_1:def 4;

      now

        let s1;

        assume that

         A4: ( rng s1) c= X and

         A5: s1 is convergent and

         A6: ( lim s1) in X;

        

         A7: (f /* s1) is convergent by A1, A4, A5, A6, Th18;

        then

         A8: (r * (f /* s1)) is convergent by NORMSP_1: 22;

        (f /. ( lim s1)) = ( lim (f /* s1)) by A1, A4, A5, A6, Th18;

        

        then ((r (#) f) /. ( lim s1)) = (r * ( lim (f /* s1))) by A3, A6, VFUNCT_1:def 4

        .= ( lim (r * (f /* s1))) by A7, NORMSP_1: 28

        .= ( lim ((r (#) f) /* s1)) by A2, A4, Th13, XBOOLE_1: 1;

        hence ((r (#) f) /* s1) is convergent & ((r (#) f) /. ( lim s1)) = ( lim ((r (#) f) /* s1)) by A2, A4, A8, Th13, XBOOLE_1: 1;

      end;

      hence thesis by A3, Th18;

    end;

    theorem :: NFCONT_1:28

    

     Th28: f is_continuous_on X implies ||.f.|| is_continuous_on X & ( - f) is_continuous_on X

    proof

      assume

       A1: f is_continuous_on X;

      thus ||.f.|| is_continuous_on X

      proof

        

         A2: X c= ( dom f) by A1;

        hence

         A3: X c= ( dom ||.f.||) by NORMSP_0:def 3;

        let r be Point of S;

        assume

         A4: r in X;

        then

         A5: (f | X) is_continuous_in r by A1;

        thus ( ||.f.|| | X) is_continuous_in r

        proof

          

           A6: r in (( dom ||.f.||) /\ X) by A3, A4, XBOOLE_0:def 4;

          hence r in ( dom ( ||.f.|| | X)) by RELAT_1: 61;

          let s1;

          assume that

           A7: ( rng s1) c= ( dom ( ||.f.|| | X)) and

           A8: s1 is convergent & ( lim s1) = r;

          ( rng s1) c= (( dom ||.f.||) /\ X) by A7, RELAT_1: 61;

          then ( rng s1) c= (( dom f) /\ X) by NORMSP_0:def 3;

          then

           A9: ( rng s1) c= ( dom (f | X)) by RELAT_1: 61;

          then

           A10: ((f | X) /. r) = ( lim ((f | X) /* s1)) by A5, A8;

          now

            let n be Element of NAT ;

            ( dom s1) = NAT by FUNCT_2:def 1;

            then

             A11: (s1 . n) in ( rng s1) by FUNCT_1: 3;

            then (s1 . n) in ( dom (f | X)) by A9;

            then

             A12: (s1 . n) in (( dom f) /\ X) by RELAT_1: 61;

            then

             A13: (s1 . n) in X by XBOOLE_0:def 4;

            (s1 . n) in ( dom f) by A12, XBOOLE_0:def 4;

            then

             A14: (s1 . n) in ( dom ||.f.||) by NORMSP_0:def 3;

            

            thus ( ||.((f | X) /* s1).|| . n) = ||.(((f | X) /* s1) . n).|| by NORMSP_0:def 4

            .= ||.((f | X) /. (s1 . n)).|| by A9, FUNCT_2: 109

            .= ||.(f /. (s1 . n)).|| by A9, A11, PARTFUN2: 15

            .= ( ||.f.|| . (s1 . n)) by A14, NORMSP_0:def 3

            .= (( ||.f.|| | X) . (s1 . n)) by A13, FUNCT_1: 49

            .= (( ||.f.|| | X) /. (s1 . n)) by A7, A11, PARTFUN1:def 6

            .= ((( ||.f.|| | X) /* s1) . n) by A7, FUNCT_2: 109;

          end;

          then

           A15: ||.((f | X) /* s1).|| = (( ||.f.|| | X) /* s1) by FUNCT_2: 63;

          

           A16: ((f | X) /* s1) is convergent by A5, A8, A9;

          hence (( ||.f.|| | X) /* s1) is convergent by A15, NORMSP_1: 23;

           ||.((f | X) /. r).|| = ||.(f /. r).|| by A2, A4, PARTFUN2: 17

          .= ( ||.f.|| . r) by A3, A4, NORMSP_0:def 3

          .= ( ||.f.|| /. r) by A3, A4, PARTFUN1:def 6

          .= (( ||.f.|| | X) /. r) by A6, PARTFUN2: 16;

          hence thesis by A16, A10, A15, LOPBAN_1: 20;

        end;

      end;

      (( - 1) (#) f) is_continuous_on X by A1, Th27;

      hence thesis by VFUNCT_1: 23;

    end;

    theorem :: NFCONT_1:29

    f is total & (for x1, x2 holds (f /. (x1 + x2)) = ((f /. x1) + (f /. x2))) & (ex x0 st f is_continuous_in x0) implies f is_continuous_on the carrier of S

    proof

      assume that

       A1: f is total and

       A2: for x1, x2 holds (f /. (x1 + x2)) = ((f /. x1) + (f /. x2));

      

       A3: ( dom f) = the carrier of S by A1, PARTFUN1:def 2;

      given x0 such that

       A4: f is_continuous_in x0;

      ((f /. x0) + ( 0. T)) = (f /. x0)

      .= (f /. (x0 + ( 0. S)))

      .= ((f /. x0) + (f /. ( 0. S))) by A2;

      then

       A5: (f /. ( 0. S)) = ( 0. T) by RLVECT_1: 8;

       A6:

      now

        let x1;

        ( 0. T) = (f /. (x1 + ( - x1))) by A5, RLVECT_1: 5

        .= ((f /. x1) + (f /. ( - x1))) by A2;

        hence ( - (f /. x1)) = (f /. ( - x1)) by RLVECT_1: 6;

      end;

       A7:

      now

        let x1, x2;

        

        thus (f /. (x1 - x2)) = ((f /. x1) + (f /. ( - x2))) by A2

        .= ((f /. x1) - (f /. x2)) by A6;

      end;

      now

        let x1;

        let r be Real;

        assume that x1 in the carrier of S and

         A8: r > 0 ;

        set y = (x1 - x0);

        consider s such that

         A9: 0 < s and

         A10: for x1 st x1 in ( dom f) & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r by A4, A8, Th7;

        take s;

        thus s > 0 by A9;

        let x2 such that x2 in the carrier of S and

         A11: ||.(x2 - x1).|| < s;

        

         A12: (y + x0) = (x1 - (x0 - x0)) by RLVECT_1: 29

        .= (x1 - ( 0. S)) by RLVECT_1: 15

        .= x1;

        then

         A13: ||.((x2 - y) - x0).|| = ||.(x2 - x1).|| by RLVECT_1: 27;

         ||.((f /. x2) - (f /. x1)).|| = ||.((f /. x2) - ((f /. y) + (f /. x0))).|| by A2, A12

        .= ||.(((f /. x2) - (f /. y)) - (f /. x0)).|| by RLVECT_1: 27

        .= ||.((f /. (x2 - y)) - (f /. x0)).|| by A7;

        hence ||.((f /. x2) - (f /. x1)).|| < r by A3, A10, A11, A13;

      end;

      hence thesis by A3, Th19;

    end;

    theorem :: NFCONT_1:30

    

     Th30: for f st ( dom f) is compact & f is_continuous_on ( dom f) holds ( rng f) is compact

    proof

      let f;

      assume that

       A1: ( dom f) is compact and

       A2: f is_continuous_on ( dom f);

      now

        let s1 be sequence of T such that

         A3: ( rng s1) c= ( rng f);

        defpred P[ set, set] means $2 in ( dom f) & (f /. $2) = (s1 . $1);

        

         A4: for n be Element of NAT holds ex p be Point of S st P[n, p]

        proof

          let n be Element of NAT ;

          ( dom s1) = NAT by FUNCT_2:def 1;

          then (s1 . n) in ( rng s1) by FUNCT_1: 3;

          then

          consider p be Point of S such that

           A5: p in ( dom f) & (s1 . n) = (f . p) by A3, PARTFUN1: 3;

          take p;

          thus thesis by A5, PARTFUN1:def 6;

        end;

        consider q1 be sequence of S such that

         A6: for n be Element of NAT holds P[n, (q1 . n)] from FUNCT_2:sch 3( A4);

        now

          let x be object;

          assume x in ( rng q1);

          then

          consider n such that

           A7: x = (q1 . n) by Th6;

          n in NAT by ORDINAL1:def 12;

          hence x in ( dom f) by A6, A7;

        end;

        then

         A8: ( rng q1) c= ( dom f);

        then

        consider s2 such that

         A9: s2 is subsequence of q1 and

         A10: s2 is convergent and

         A11: ( lim s2) in ( dom f) by A1;

        take q2 = (f /* s2);

        ( rng s2) c= ( rng q1) by A9, VALUED_0: 21;

        then

         A12: ( rng s2) c= ( dom f) by A8;

        now

          let n be Element of NAT ;

          (f /. (q1 . n)) = (s1 . n) by A6;

          hence ((f /* q1) . n) = (s1 . n) by A8, FUNCT_2: 109;

        end;

        then

         A13: (f /* q1) = s1 by FUNCT_2: 63;

        (f | ( dom f)) is_continuous_in ( lim s2) by A2, A11;

        then

         A14: f is_continuous_in ( lim s2) by RELAT_1: 68;

        then (f /. ( lim s2)) = ( lim (f /* s2)) by A10, A12;

        hence q2 is subsequence of s1 & q2 is convergent & ( lim q2) in ( rng f) by A8, A13, A9, A10, A14, A12, PARTFUN2: 2, VALUED_0: 22;

      end;

      hence thesis;

    end;

    theorem :: NFCONT_1:31

    

     Th31: for f be PartFunc of the carrier of S, REAL st ( dom f) is compact & f is_continuous_on ( dom f) holds ( rng f) is compact

    proof

      let f be PartFunc of the carrier of S, REAL ;

      assume that

       A1: ( dom f) is compact and

       A2: f is_continuous_on ( dom f);

      now

        let s1 be Real_Sequence such that

         A3: ( rng s1) c= ( rng f);

        defpred P[ set, set] means $2 in ( dom f) & (f /. $2) = (s1 . $1);

        

         A4: for n be Element of NAT holds ex p be Point of S st P[n, p]

        proof

          let n be Element of NAT ;

          ( dom s1) = NAT by FUNCT_2:def 1;

          then (s1 . n) in ( rng s1) by FUNCT_1: 3;

          then

          consider p be Point of S such that

           A5: p in ( dom f) & (s1 . n) = (f . p) by A3, PARTFUN1: 3;

          take p;

          thus thesis by A5, PARTFUN1:def 6;

        end;

        consider q1 be sequence of S such that

         A6: for n be Element of NAT holds P[n, (q1 . n)] from FUNCT_2:sch 3( A4);

        now

          let x be object;

          assume x in ( rng q1);

          then

          consider n such that

           A7: x = (q1 . n) by Th6;

          n in NAT by ORDINAL1:def 12;

          hence x in ( dom f) by A6, A7;

        end;

        then

         A8: ( rng q1) c= ( dom f);

        then

        consider s2 such that

         A9: s2 is subsequence of q1 and

         A10: s2 is convergent and

         A11: ( lim s2) in ( dom f) by A1;

        take q2 = (f /* s2);

        ( rng s2) c= ( rng q1) by A9, VALUED_0: 21;

        then

         A12: ( rng s2) c= ( dom f) by A8;

        now

          let n be Element of NAT ;

          (f /. (q1 . n)) = (s1 . n) by A6;

          hence ((f /* q1) . n) = (s1 . n) by A8, FUNCT_2: 109;

        end;

        then

         A13: (f /* q1) = s1 by FUNCT_2: 63;

        (f | ( dom f)) is_continuous_in ( lim s2) by A2, A11;

        then

         A14: f is_continuous_in ( lim s2) by RELAT_1: 68;

        then (f /. ( lim s2)) = ( lim (f /* s2)) by A10, A12;

        hence q2 is subsequence of s1 & q2 is convergent & ( lim q2) in ( rng f) by A8, A13, A9, A10, A14, A12, PARTFUN2: 2, VALUED_0: 22;

      end;

      hence thesis by RCOMP_1:def 3;

    end;

    theorem :: NFCONT_1:32

    Y c= ( dom f) & Y is compact & f is_continuous_on Y implies (f .: Y) is compact

    proof

      assume that

       A1: Y c= ( dom f) and

       A2: Y is compact and

       A3: f is_continuous_on Y;

      

       A4: ( dom (f | Y)) = (( dom f) /\ Y) by RELAT_1: 61

      .= Y by A1, XBOOLE_1: 28;

      (f | Y) is_continuous_on Y

      proof

        thus Y c= ( dom (f | Y)) by A4;

        let r be Point of S;

        assume r in Y;

        then (f | Y) is_continuous_in r by A3;

        hence thesis by RELAT_1: 72;

      end;

      then ( rng (f | Y)) is compact by A2, A4, Th30;

      hence thesis by RELAT_1: 115;

    end;

    theorem :: NFCONT_1:33

    

     Th33: for f be PartFunc of the carrier of S, REAL st ( dom f) <> {} & ( dom f) is compact & f is_continuous_on ( dom f) holds ex x1, x2 st x1 in ( dom f) & x2 in ( dom f) & (f /. x1) = ( upper_bound ( rng f)) & (f /. x2) = ( lower_bound ( rng f))

    proof

      let f be PartFunc of the carrier of S, REAL ;

      assume ( dom f) <> {} & ( dom f) is compact & f is_continuous_on ( dom f);

      then

       A1: ( rng f) <> {} & ( rng f) is compact by Th31, RELAT_1: 42;

      then

      consider x be Element of S such that

       A2: x in ( dom f) & ( upper_bound ( rng f)) = (f . x) by PARTFUN1: 3, RCOMP_1: 14;

      take x;

      consider y be Element of S such that

       A3: y in ( dom f) & ( lower_bound ( rng f)) = (f . y) by A1, PARTFUN1: 3, RCOMP_1: 14;

      take y;

      thus thesis by A2, A3, PARTFUN1:def 6;

    end;

    theorem :: NFCONT_1:34

    

     Th34: for f st ( dom f) <> {} & ( dom f) is compact & f is_continuous_on ( dom f) holds ex x1, x2 st x1 in ( dom f) & x2 in ( dom f) & ( ||.f.|| /. x1) = ( upper_bound ( rng ||.f.||)) & ( ||.f.|| /. x2) = ( lower_bound ( rng ||.f.||))

    proof

      let f such that

       A1: ( dom f) <> {} and

       A2: ( dom f) is compact and

       A3: f is_continuous_on ( dom f);

      

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

      ( dom ||.f.||) is compact by A2, NORMSP_0:def 3;

      then

       A5: ( rng ||.f.||) is compact by A3, A4, Th28, Th31;

      

       A6: ( rng ||.f.||) <> {} by A1, A4, RELAT_1: 42;

      then

      consider x be Element of S such that

       A7: x in ( dom ||.f.||) & ( upper_bound ( rng ||.f.||)) = ( ||.f.|| . x) by A5, PARTFUN1: 3, RCOMP_1: 14;

      consider y be Element of S such that

       A8: y in ( dom ||.f.||) & ( lower_bound ( rng ||.f.||)) = ( ||.f.|| . y) by A6, A5, PARTFUN1: 3, RCOMP_1: 14;

      take x;

      take y;

      thus thesis by A7, A8, NORMSP_0:def 3, PARTFUN1:def 6;

    end;

    theorem :: NFCONT_1:35

    

     Th35: ( ||.f.|| | X) = ||.(f | X).||

    proof

      

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

      .= (( dom f) /\ X) by NORMSP_0:def 3

      .= ( dom (f | X)) by RELAT_1: 61

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

      now

        let c be Point of S;

        assume

         A2: c in ( dom ( ||.f.|| | X));

        then

         A3: c in ( dom (f | X)) by A1, NORMSP_0:def 3;

        c in (( dom ||.f.||) /\ X) by A2, RELAT_1: 61;

        then

         A4: c in ( dom ||.f.||) by XBOOLE_0:def 4;

        

        thus (( ||.f.|| | X) . c) = ( ||.f.|| . c) by A2, FUNCT_1: 47

        .= ||.(f /. c).|| by A4, NORMSP_0:def 3

        .= ||.((f | X) /. c).|| by A3, PARTFUN2: 15

        .= ( ||.(f | X).|| . c) by A1, A2, NORMSP_0:def 3;

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: NFCONT_1:36

    for f, Y st Y <> {} & Y c= ( dom f) & Y is compact & f is_continuous_on Y holds ex x1, x2 st x1 in Y & x2 in Y & ( ||.f.|| /. x1) = ( upper_bound ( ||.f.|| .: Y)) & ( ||.f.|| /. x2) = ( lower_bound ( ||.f.|| .: Y))

    proof

      let f, Y such that

       A1: Y <> {} and

       A2: Y c= ( dom f) and

       A3: Y is compact and

       A4: f is_continuous_on Y;

      

       A5: ( dom (f | Y)) = (( dom f) /\ Y) by RELAT_1: 61

      .= Y by A2, XBOOLE_1: 28;

      (f | Y) is_continuous_on Y

      proof

        thus Y c= ( dom (f | Y)) by A5;

        let r be Point of S;

        assume r in Y;

        then (f | Y) is_continuous_in r by A4;

        hence thesis by RELAT_1: 72;

      end;

      then

      consider x1, x2 such that

       A6: x1 in ( dom (f | Y)) and

       A7: x2 in ( dom (f | Y)) and

       A8: ( ||.(f | Y).|| /. x1) = ( upper_bound ( rng ||.(f | Y).||)) & ( ||.(f | Y).|| /. x2) = ( lower_bound ( rng ||.(f | Y).||)) by A1, A3, A5, Th34;

      

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

      take x1, x2;

      thus x1 in Y & x2 in Y by A5, A6, A7;

      

       A10: ( ||.f.|| .: Y) = ( rng ( ||.f.|| | Y)) by RELAT_1: 115

      .= ( rng ||.(f | Y).||) by Th35;

      

       A11: x2 in ( dom ||.(f | Y).||) by A7, NORMSP_0:def 3;

      

      then

       A12: ( ||.(f | Y).|| /. x2) = ( ||.(f | Y).|| . x2) by PARTFUN1:def 6

      .= ||.((f | Y) /. x2).|| by A11, NORMSP_0:def 3

      .= ||.(f /. x2).|| by A7, PARTFUN2: 15

      .= ( ||.f.|| . x2) by A2, A5, A7, A9, NORMSP_0:def 3

      .= ( ||.f.|| /. x2) by A2, A5, A7, A9, PARTFUN1:def 6;

      

       A13: x1 in ( dom ||.(f | Y).||) by A6, NORMSP_0:def 3;

      

      then ( ||.(f | Y).|| /. x1) = ( ||.(f | Y).|| . x1) by PARTFUN1:def 6

      .= ||.((f | Y) /. x1).|| by A13, NORMSP_0:def 3

      .= ||.(f /. x1).|| by A6, PARTFUN2: 15

      .= ( ||.f.|| . x1) by A2, A5, A6, A9, NORMSP_0:def 3

      .= ( ||.f.|| /. x1) by A2, A5, A6, A9, PARTFUN1:def 6;

      hence thesis by A8, A12, A10;

    end;

    theorem :: NFCONT_1:37

    for f be PartFunc of the carrier of S, REAL holds for Y st Y <> {} & Y c= ( dom f) & Y is compact & f is_continuous_on Y holds ex x1, x2 st x1 in Y & x2 in Y & (f /. x1) = ( upper_bound (f .: Y)) & (f /. x2) = ( lower_bound (f .: Y))

    proof

      let f be PartFunc of the carrier of S, REAL ;

      let Y such that

       A1: Y <> {} and

       A2: Y c= ( dom f) and

       A3: Y is compact and

       A4: f is_continuous_on Y;

      

       A5: ( dom (f | Y)) = (( dom f) /\ Y) by RELAT_1: 61

      .= Y by A2, XBOOLE_1: 28;

      (f | Y) is_continuous_on Y

      proof

        thus Y c= ( dom (f | Y)) by A5;

        let r be Point of S;

        assume r in Y;

        then (f | Y) is_continuous_in r by A4;

        hence thesis by RELAT_1: 72;

      end;

      then

      consider x1, x2 such that

       A6: x1 in ( dom (f | Y)) & x2 in ( dom (f | Y)) and

       A7: ((f | Y) /. x1) = ( upper_bound ( rng (f | Y))) & ((f | Y) /. x2) = ( lower_bound ( rng (f | Y))) by A1, A3, A5, Th33;

      take x1, x2;

      thus x1 in Y & x2 in Y by A5, A6;

      ((f | Y) /. x1) = (f /. x1) & ((f | Y) /. x2) = (f /. x2) by A6, PARTFUN2: 15;

      hence thesis by A7, RELAT_1: 115;

    end;

    definition

      let S, T;

      let X, f;

      :: NFCONT_1:def9

      pred f is_Lipschitzian_on X means X c= ( dom f) & ex r st 0 < r & for x1, x2 st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= (r * ||.(x1 - x2).||);

    end

    definition

      let S;

      let X;

      let f be PartFunc of the carrier of S, REAL ;

      :: NFCONT_1:def10

      pred f is_Lipschitzian_on X means X c= ( dom f) & ex r st 0 < r & for x1, x2 st x1 in X & x2 in X holds |.((f /. x1) - (f /. x2)).| <= (r * ||.(x1 - x2).||);

    end

    theorem :: NFCONT_1:38

    

     Th38: f is_Lipschitzian_on X & X1 c= X implies f is_Lipschitzian_on X1

    proof

      assume that

       A1: f is_Lipschitzian_on X and

       A2: X1 c= X;

      X c= ( dom f) by A1;

      hence X1 c= ( dom f) by A2;

      consider s such that

       A3: 0 < s and

       A4: for x1, x2 st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= (s * ||.(x1 - x2).||) by A1;

      take s;

      thus 0 < s by A3;

      let x1, x2;

      assume x1 in X1 & x2 in X1;

      hence thesis by A2, A4;

    end;

    theorem :: NFCONT_1:39

    f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 implies (f1 + f2) is_Lipschitzian_on (X /\ X1)

    proof

      assume that

       A1: f1 is_Lipschitzian_on X and

       A2: f2 is_Lipschitzian_on X1;

      

       A3: f1 is_Lipschitzian_on (X /\ X1) by A1, Th38, XBOOLE_1: 17;

      then

      consider s such that

       A4: 0 < s and

       A5: for x1, x2 st x1 in (X /\ X1) & x2 in (X /\ X1) holds ||.((f1 /. x1) - (f1 /. x2)).|| <= (s * ||.(x1 - x2).||);

      

       A6: f2 is_Lipschitzian_on (X /\ X1) by A2, Th38, XBOOLE_1: 17;

      then

       A7: (X /\ X1) c= ( dom f2);

      (X /\ X1) c= ( dom f1) by A3;

      then (X /\ X1) c= (( dom f1) /\ ( dom f2)) by A7, XBOOLE_1: 19;

      hence

       A8: (X /\ X1) c= ( dom (f1 + f2)) by VFUNCT_1:def 1;

      consider g such that

       A9: 0 < g and

       A10: for x1, x2 st x1 in (X /\ X1) & x2 in (X /\ X1) holds ||.((f2 /. x1) - (f2 /. x2)).|| <= (g * ||.(x1 - x2).||) by A6;

      take p = (s + g);

      ( 0 + 0 ) < (s + g) by A4, A9;

      hence 0 < p;

      let x1, x2;

      assume that

       A11: x1 in (X /\ X1) and

       A12: x2 in (X /\ X1);

      

       A13: ||.((f2 /. x1) - (f2 /. x2)).|| <= (g * ||.(x1 - x2).||) by A10, A11, A12;

       ||.((f1 /. x1) - (f1 /. x2)).|| <= (s * ||.(x1 - x2).||) by A5, A11, A12;

      then

       A14: ( ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).||) <= ((s * ||.(x1 - x2).||) + (g * ||.(x1 - x2).||)) by A13, XREAL_1: 7;

       ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| = ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 + f2) /. x2)).|| by A8, A11, VFUNCT_1:def 1

      .= ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 /. x2) + (f2 /. x2))).|| by A8, A12, VFUNCT_1:def 1

      .= ||.((f1 /. x1) + ((f2 /. x1) - ((f1 /. x2) + (f2 /. x2)))).|| by RLVECT_1:def 3

      .= ||.((f1 /. x1) + (((f2 /. x1) - (f1 /. x2)) - (f2 /. x2))).|| by RLVECT_1: 27

      .= ||.((f1 /. x1) + ((( - (f1 /. x2)) + (f2 /. x1)) - (f2 /. x2))).||

      .= ||.((f1 /. x1) + (( - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def 3

      .= ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:def 3;

      then ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= ( ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).||) by NORMSP_1:def 1;

      hence thesis by A14, XXREAL_0: 2;

    end;

    theorem :: NFCONT_1:40

    f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 implies (f1 - f2) is_Lipschitzian_on (X /\ X1)

    proof

      assume that

       A1: f1 is_Lipschitzian_on X and

       A2: f2 is_Lipschitzian_on X1;

      

       A3: f1 is_Lipschitzian_on (X /\ X1) by A1, Th38, XBOOLE_1: 17;

      then

      consider s such that

       A4: 0 < s and

       A5: for x1, x2 st x1 in (X /\ X1) & x2 in (X /\ X1) holds ||.((f1 /. x1) - (f1 /. x2)).|| <= (s * ||.(x1 - x2).||);

      

       A6: f2 is_Lipschitzian_on (X /\ X1) by A2, Th38, XBOOLE_1: 17;

      then

       A7: (X /\ X1) c= ( dom f2);

      (X /\ X1) c= ( dom f1) by A3;

      then (X /\ X1) c= (( dom f1) /\ ( dom f2)) by A7, XBOOLE_1: 19;

      hence

       A8: (X /\ X1) c= ( dom (f1 - f2)) by VFUNCT_1:def 2;

      consider g such that

       A9: 0 < g and

       A10: for x1, x2 st x1 in (X /\ X1) & x2 in (X /\ X1) holds ||.((f2 /. x1) - (f2 /. x2)).|| <= (g * ||.(x1 - x2).||) by A6;

      take p = (s + g);

      ( 0 + 0 ) < (s + g) by A4, A9;

      hence 0 < p;

      let x1, x2;

      assume that

       A11: x1 in (X /\ X1) and

       A12: x2 in (X /\ X1);

      

       A13: ||.((f2 /. x1) - (f2 /. x2)).|| <= (g * ||.(x1 - x2).||) by A10, A11, A12;

       ||.((f1 /. x1) - (f1 /. x2)).|| <= (s * ||.(x1 - x2).||) by A5, A11, A12;

      then

       A14: ( ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).||) <= ((s * ||.(x1 - x2).||) + (g * ||.(x1 - x2).||)) by A13, XREAL_1: 7;

       ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| = ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 - f2) /. x2)).|| by A8, A11, VFUNCT_1:def 2

      .= ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).|| by A8, A12, VFUNCT_1:def 2

      .= ||.((f1 /. x1) - ((f2 /. x1) + ((f1 /. x2) - (f2 /. x2)))).|| by RLVECT_1: 27

      .= ||.((f1 /. x1) - (((f1 /. x2) + (f2 /. x1)) - (f2 /. x2))).|| by RLVECT_1:def 3

      .= ||.((f1 /. x1) - ((f1 /. x2) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def 3

      .= ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1: 27;

      then ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= ( ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).||) by NORMSP_1: 3;

      hence thesis by A14, XXREAL_0: 2;

    end;

    theorem :: NFCONT_1:41

    

     Th41: f is_Lipschitzian_on X implies (p (#) f) is_Lipschitzian_on X

    proof

      assume

       A1: f is_Lipschitzian_on X;

      then

      consider s such that

       A2: 0 < s and

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

      X c= ( dom f) by A1;

      hence

       A4: X c= ( dom (p (#) f)) by VFUNCT_1:def 4;

      per cases ;

        suppose

         A5: p = 0 ;

        take s;

        thus 0 < s by A2;

        let x1, x2;

        assume that

         A6: x1 in X and

         A7: x2 in X;

         0 <= ||.(x1 - x2).|| by NORMSP_1: 4;

        then

         A8: (s * 0 ) <= (s * ||.(x1 - x2).||) by A2;

         ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| = ||.((p * (f /. x1)) - ((p (#) f) /. x2)).|| by A4, A6, VFUNCT_1:def 4

        .= ||.(( 0. T) - ((p (#) f) /. x2)).|| by A5, RLVECT_1: 10

        .= ||.(( 0. T) - (p * (f /. x2))).|| by A4, A7, VFUNCT_1:def 4

        .= ||.(( 0. T) - ( 0. T)).|| by A5, RLVECT_1: 10

        .= ||.( 0. T).||

        .= 0 by NORMSP_1: 1;

        hence ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= (s * ||.(x1 - x2).||) by A8;

      end;

        suppose

         A9: p <> 0 ;

        take g = ( |.p.| * s);

         0 < |.p.| by A9, COMPLEX1: 47;

        then ( 0 * s) < ( |.p.| * s) by A2, XREAL_1: 68;

        hence 0 < g;

        let x1, x2;

        assume that

         A10: x1 in X and

         A11: x2 in X;

         0 <= |.p.| by COMPLEX1: 46;

        then

         A12: ( |.p.| * ||.((f /. x1) - (f /. x2)).||) <= ( |.p.| * (s * ||.(x1 - x2).||)) by A3, A10, A11, XREAL_1: 64;

         ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| = ||.((p * (f /. x1)) - ((p (#) f) /. x2)).|| by A4, A10, VFUNCT_1:def 4

        .= ||.((p * (f /. x1)) - (p * (f /. x2))).|| by A4, A11, VFUNCT_1:def 4

        .= ||.(p * ((f /. x1) - (f /. x2))).|| by RLVECT_1: 34

        .= ( |.p.| * ||.((f /. x1) - (f /. x2)).||) by NORMSP_1:def 1;

        hence ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= (g * ||.(x1 - x2).||) by A12;

      end;

    end;

    theorem :: NFCONT_1:42

    f is_Lipschitzian_on X implies ( - f) is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X

    proof

      assume

       A1: f is_Lipschitzian_on X;

      then

      consider s such that

       A2: 0 < s and

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

      ( - f) = (( - 1) (#) f) by VFUNCT_1: 23;

      hence ( - f) is_Lipschitzian_on X by A1, Th41;

      X c= ( dom f) by A1;

      hence

       A4: X c= ( dom ||.f.||) by NORMSP_0:def 3;

      take s;

      thus 0 < s by A2;

      let x1, x2;

      assume that

       A5: x1 in X and

       A6: x2 in X;

       |.(( ||.f.|| /. x1) - ( ||.f.|| /. x2)).| = |.(( ||.f.|| . x1) - ( ||.f.|| /. x2)).| by A4, A5, PARTFUN1:def 6

      .= |.(( ||.f.|| . x1) - ( ||.f.|| . x2)).| by A4, A6, PARTFUN1:def 6

      .= |.( ||.(f /. x1).|| - ( ||.f.|| . x2)).| by A4, A5, NORMSP_0:def 3

      .= |.( ||.(f /. x1).|| - ||.(f /. x2).||).| by A4, A6, NORMSP_0:def 3;

      then

       A7: |.(( ||.f.|| /. x1) - ( ||.f.|| /. x2)).| <= ||.((f /. x1) - (f /. x2)).|| by NORMSP_1: 9;

       ||.((f /. x1) - (f /. x2)).|| <= (s * ||.(x1 - x2).||) by A3, A5, A6;

      hence thesis by A7, XXREAL_0: 2;

    end;

    theorem :: NFCONT_1:43

    

     Th43: X c= ( dom f) & (f | X) is constant implies f is_Lipschitzian_on X

    proof

      assume that

       A1: X c= ( dom f) and

       A2: (f | X) is constant;

      now

        let x1, x2;

        assume that

         A3: x1 in X and

         A4: x2 in X;

        

         A5: x1 in (X /\ ( dom f)) & x2 in (X /\ ( dom f)) by A1, A3, A4, XBOOLE_0:def 4;

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

        .= (f . x2) by A2, A5, PARTFUN2: 58

        .= (f /. x2) by A1, A4, PARTFUN1:def 6;

        

        then ||.((f /. x1) - (f /. x2)).|| = ||.( 0. T).|| by RLVECT_1: 15

        .= 0 by NORMSP_1: 1;

        hence ||.((f /. x1) - (f /. x2)).|| <= (1 * ||.(x1 - x2).||) by NORMSP_1: 4;

      end;

      hence thesis by A1;

    end;

    theorem :: NFCONT_1:44

    ( id Y) is_Lipschitzian_on Y

    proof

      reconsider r = 1 as Real;

      thus Y c= ( dom ( id Y)) by RELAT_1: 45;

      take r;

      thus r > 0 ;

      let x1, x2;

      assume that

       A1: x1 in Y and

       A2: x2 in Y;

       ||.((( id Y) /. x1) - (( id Y) /. x2)).|| = ||.(x1 - (( id Y) /. x2)).|| by A1, PARTFUN2: 6

      .= (r * ||.(x1 - x2).||) by A2, PARTFUN2: 6;

      hence thesis;

    end;

    theorem :: NFCONT_1:45

    

     Th45: f is_Lipschitzian_on X implies f is_continuous_on X

    proof

      assume

       A1: f is_Lipschitzian_on X;

      then

      consider r such that

       A2: 0 < r and

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

      

       A4: X c= ( dom f) by A1;

      then

       A5: ( dom (f | X)) = X by RELAT_1: 62;

      now

        let x0 such that

         A6: x0 in X;

        now

          let g such that

           A7: 0 < g;

          reconsider s = (g / r) as Real;

          take s9 = s;

           A8:

          now

            let x1;

            assume that

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

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

            (r * ||.(x1 - x0).||) < ((g / r) * r) by A2, A10, XREAL_1: 68;

            then

             A11: (r * ||.(x1 - x0).||) < g by A2, XCMPLX_1: 87;

             ||.((f /. x1) - (f /. x0)).|| <= (r * ||.(x1 - x0).||) by A3, A5, A6, A9;

            then ||.((f /. x1) - (f /. x0)).|| < g by A11, XXREAL_0: 2;

            then ||.(((f | X) /. x1) - (f /. x0)).|| < g by A9, PARTFUN2: 15;

            hence ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g by A5, A6, PARTFUN2: 15;

          end;

           0 < (r " ) & s9 = (g * (r " )) by A2, XCMPLX_0:def 9;

          hence 0 < s9 & for x1 st x1 in ( dom (f | X)) & ||.(x1 - x0).|| < s9 holds ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g by A7, A8, XREAL_1: 129;

        end;

        hence (f | X) is_continuous_in x0 by A5, A6, Th7;

      end;

      hence thesis by A4;

    end;

    theorem :: NFCONT_1:46

    

     Th46: for f be PartFunc of the carrier of S, REAL st f is_Lipschitzian_on X holds f is_continuous_on X

    proof

      let f be PartFunc of the carrier of S, REAL ;

      assume

       A1: f is_Lipschitzian_on X;

      then

      consider r such that

       A2: 0 < r and

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

      

       A4: X c= ( dom f) by A1;

      then

       A5: ( dom (f | X)) = X by RELAT_1: 62;

      now

        let x0 such that

         A6: x0 in X;

        now

          let g such that

           A7: 0 < g;

          reconsider s = (g / r) as Real;

          take s9 = s;

           A8:

          now

            let x1;

            assume that

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

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

            (r * ||.(x1 - x0).||) < ((g / r) * r) by A2, A10, XREAL_1: 68;

            then

             A11: (r * ||.(x1 - x0).||) < g by A2, XCMPLX_1: 87;

             |.((f /. x1) - (f /. x0)).| <= (r * ||.(x1 - x0).||) by A3, A5, A6, A9;

            then |.((f /. x1) - (f /. x0)).| < g by A11, XXREAL_0: 2;

            then |.(((f | X) /. x1) - (f /. x0)).| < g by A9, PARTFUN2: 15;

            hence |.(((f | X) /. x1) - ((f | X) /. x0)).| < g by A5, A6, PARTFUN2: 15;

          end;

           0 < (r " ) & s9 = (g * (r " )) by A2, XCMPLX_0:def 9;

          hence 0 < s9 & for x1 st x1 in ( dom (f | X)) & ||.(x1 - x0).|| < s9 holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < g by A7, A8, XREAL_1: 129;

        end;

        hence (f | X) is_continuous_in x0 by A5, A6, Th8;

      end;

      hence thesis by A4;

    end;

    theorem :: NFCONT_1:47

    for f st (ex r be Point of T st ( rng f) = {r}) holds f is_continuous_on ( dom f)

    proof

      let f;

      given r be Point of T such that

       A1: ( rng f) = {r};

      now

        let x1, x2;

        assume that

         A2: x1 in ( dom f) and

         A3: x2 in ( dom f);

        (f . x2) in ( rng f) by A3, FUNCT_1:def 3;

        then (f /. x2) in ( rng f) by A3, PARTFUN1:def 6;

        then

         A4: (f /. x2) = r by A1, TARSKI:def 1;

        (f . x1) in ( rng f) by A2, FUNCT_1:def 3;

        then (f /. x1) in ( rng f) by A2, PARTFUN1:def 6;

        then (f /. x1) = r by A1, TARSKI:def 1;

        

        then ||.((f /. x1) - (f /. x2)).|| = ||.( 0. T).|| by A4, RLVECT_1: 15

        .= 0 by NORMSP_1: 1;

        hence ||.((f /. x1) - (f /. x2)).|| <= (1 * ||.(x1 - x2).||) by NORMSP_1: 4;

      end;

      then f is_Lipschitzian_on ( dom f);

      hence thesis by Th45;

    end;

    theorem :: NFCONT_1:48

    X c= ( dom f) & (f | X) is constant implies f is_continuous_on X by Th43, Th45;

    theorem :: NFCONT_1:49

    

     Th49: for f be PartFunc of S, S st (for x0 st x0 in ( dom f) holds (f /. x0) = x0) holds f is_continuous_on ( dom f)

    proof

      let f be PartFunc of S, S such that

       A1: for x0 st x0 in ( dom f) holds (f /. x0) = x0;

      now

        let x1, x2;

        assume that

         A2: x1 in ( dom f) and

         A3: x2 in ( dom f);

        (f /. x1) = x1 by A1, A2;

        hence ||.((f /. x1) - (f /. x2)).|| <= (1 * ||.(x1 - x2).||) by A1, A3;

      end;

      then f is_Lipschitzian_on ( dom f);

      hence thesis by Th45;

    end;

    theorem :: NFCONT_1:50

    for f be PartFunc of S, S st f = ( id ( dom f)) holds f is_continuous_on ( dom f)

    proof

      let f be PartFunc of S, S;

      assume

       A1: f = ( id ( dom f));

      now

        let x0 such that

         A2: x0 in ( dom f);

        

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

        .= x0 by A1, A2, FUNCT_1: 17;

      end;

      hence thesis by Th49;

    end;

    theorem :: NFCONT_1:51

    for f be PartFunc of S, S st Y c= ( dom f) & (f | Y) = ( id Y) holds f is_continuous_on Y

    proof

      let f be PartFunc of S, S;

      assume that

       A1: Y c= ( dom f) and

       A2: (f | Y) = ( id Y);

      now

        let x1, x2;

        assume that

         A3: x1 in Y and

         A4: x2 in Y;

        x1 in (( dom f) /\ Y) by A1, A3, XBOOLE_0:def 4;

        then

         A5: x1 in ( dom (f | Y)) by RELAT_1: 61;

        ((f | Y) . x1) = x1 by A2, A3, FUNCT_1: 17;

        then (f . x1) = x1 by A5, FUNCT_1: 47;

        then

         A6: (f /. x1) = x1 by A1, A3, PARTFUN1:def 6;

        x2 in (( dom f) /\ Y) by A1, A4, XBOOLE_0:def 4;

        then

         A7: x2 in ( dom (f | Y)) by RELAT_1: 61;

        ((f | Y) . x2) = x2 by A2, A4, FUNCT_1: 17;

        then (f . x2) = x2 by A7, FUNCT_1: 47;

        hence ||.((f /. x1) - (f /. x2)).|| <= (1 * ||.(x1 - x2).||) by A1, A4, A6, PARTFUN1:def 6;

      end;

      then f is_Lipschitzian_on Y by A1;

      hence thesis by Th45;

    end;

    theorem :: NFCONT_1:52

    for f be PartFunc of S, S holds for r be Real holds for p be Point of S holds (X c= ( dom f) & (for x0 st x0 in X holds (f /. x0) = ((r * x0) + p)) implies f is_continuous_on X)

    proof

      let f be PartFunc of S, S;

      let r be Real;

      let p be Point of S;

      assume that

       A1: X c= ( dom f) and

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

      now

        ( 0 + 0 ) < ( |.r.| + 1) by COMPLEX1: 46, XREAL_1: 8;

        hence 0 < ( |.r.| + 1);

        let x1,x2 be Point of S;

        assume x1 in X & x2 in X;

        then (f /. x1) = ((r * x1) + p) & (f /. x2) = ((r * x2) + p) by A2;

        

        then

         A3: ||.((f /. x1) - (f /. x2)).|| = ||.((r * x1) + (p - (p + (r * x2)))).|| by RLVECT_1:def 3

        .= ||.((r * x1) + ((p - p) - (r * x2))).|| by RLVECT_1: 27

        .= ||.((r * x1) + (( 0. S) - (r * x2))).|| by RLVECT_1: 15

        .= ||.((r * x1) - (r * x2)).||

        .= ||.(r * (x1 - x2)).|| by RLVECT_1: 34

        .= ( |.r.| * ||.(x1 - x2).||) by NORMSP_1:def 1;

         0 <= ||.(x1 - x2).|| by NORMSP_1: 4;

        then ( ||.((f /. x1) - (f /. x2)).|| + 0 ) <= (( |.r.| * ||.(x1 - x2).||) + (1 * ||.(x1 - x2).||)) by A3, XREAL_1: 7;

        hence ||.((f /. x1) - (f /. x2)).|| <= (( |.r.| + 1) * ||.(x1 - x2).||);

      end;

      then f is_Lipschitzian_on X by A1;

      hence thesis by Th45;

    end;

    theorem :: NFCONT_1:53

    

     Th53: for f be PartFunc of the carrier of S, REAL st (for x0 st x0 in ( dom f) holds (f /. x0) = ||.x0.||) holds f is_continuous_on ( dom f)

    proof

      let f be PartFunc of the carrier of S, REAL ;

      assume

       A1: for x0 st x0 in ( dom f) holds (f /. x0) = ||.x0.||;

      now

        let x1, x2;

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

        then (f /. x1) = ||.x1.|| & (f /. x2) = ||.x2.|| by A1;

        hence |.((f /. x1) - (f /. x2)).| <= (1 * ||.(x1 - x2).||) by NORMSP_1: 9;

      end;

      then f is_Lipschitzian_on ( dom f);

      hence thesis by Th46;

    end;

    theorem :: NFCONT_1:54

    for f be PartFunc of the carrier of S, REAL st X c= ( dom f) & (for x0 st x0 in X holds (f /. x0) = ||.x0.||) holds f is_continuous_on X

    proof

      let f be PartFunc of the carrier of S, REAL ;

      assume that

       A1: X c= ( dom f) and

       A2: for x0 st x0 in X holds (f /. x0) = ||.x0.||;

      X = (( dom f) /\ X) by A1, XBOOLE_1: 28;

      then

       A3: X = ( dom (f | X)) by RELAT_1: 61;

      now

        let x0;

        assume

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

        

        hence ((f | X) /. x0) = (f /. x0) by PARTFUN2: 15

        .= ||.x0.|| by A2, A3, A4;

      end;

      then (f | X) is_continuous_on X by A3, Th53;

      hence thesis by Th22;

    end;