nfcont_3.miz



    begin

    reserve n,m,k for Nat;

    reserve x,X,X1 for set;

    reserve r,p for Real;

    reserve s,g,x0,x1,x2 for Real;

    reserve S,T for RealNormSpace;

    reserve f,f1,f2 for PartFunc of REAL , the carrier of S;

    reserve s1,s2 for Real_Sequence;

    reserve Y for Subset of REAL ;

    theorem :: NFCONT_3:1

    

     Th1: for seq be Real_Sequence, h be PartFunc of REAL , the carrier of S st ( rng seq) c= ( dom h) holds (seq . n) in ( dom h)

    proof

      let seq be Real_Sequence;

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

      n in NAT by ORDINAL1:def 12;

      then

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

      assume ( rng seq) c= ( dom h);

      then n in ( dom (h qua Function * seq)) by A1, RELAT_1: 27;

      hence thesis by FUNCT_1: 11;

    end;

    theorem :: NFCONT_3:2

    

     Th2: for h1,h2 be PartFunc of REAL , the carrier of S holds for seq be Real_Sequence 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 REAL , the carrier of S;

      let seq be Real_Sequence;

      

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

      assume

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

      now

        let n be Nat;

        

         A3: n in NAT by ORDINAL1:def 12;

        

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

        

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

        then

         A6: (seq . n) in ( dom (h1 + h2)) by Th1;

        

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

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

      end;

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

      now

        let n be Nat;

        

         A7: n in NAT by ORDINAL1:def 12;

        

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

        

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

        then

         A10: (seq . n) in ( dom (h1 - h2)) by Th1;

        

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

        .= (((h1 /* seq) . n) - ((h2 /* seq) . n)) by A8, A10, VFUNCT_1:def 2;

      end;

      hence thesis by NORMSP_1:def 3;

    end;

    theorem :: NFCONT_3:3

    for h be sequence of S, r be Real holds (r (#) h) = (r * h)

    proof

      let h be sequence of S;

      let r be Real;

      

       A1: ( dom h) = NAT by FUNCT_2:def 1;

      then

       A2: ( dom (r (#) h)) = NAT by VFUNCT_1:def 4;

      now

        let n;

        

         A3: n in NAT by ORDINAL1:def 12;

        then ((r (#) h) . n) = ((r (#) h) /. n) by A2, PARTFUN1:def 6;

        then ((r (#) h) . n) = (r * (h /. n)) by A2, VFUNCT_1:def 4, A3;

        hence ((r (#) h) . n) = (r * (h . n)) by A3, PARTFUN1:def 6, A1;

      end;

      hence thesis by NORMSP_1:def 5;

    end;

    theorem :: NFCONT_3:4

    

     Th4: for h be PartFunc of REAL , the carrier of S, seq be Real_Sequence, r be Real st ( rng seq) c= ( dom h) holds ((r (#) h) /* seq) = (r * (h /* seq))

    proof

      let h be PartFunc of REAL , the carrier of S, seq be Real_Sequence, 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;

        

         A3: n in NAT by ORDINAL1:def 12;

        

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

        

        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;

    theorem :: NFCONT_3:5

    

     Th5: for h be PartFunc of REAL , the carrier of S, seq be Real_Sequence st ( rng seq) c= ( dom h) holds ||.(h /* seq).|| = ( ||.h.|| /* seq) & ( - (h /* seq)) = (( - h) /* seq)

    proof

      let h be PartFunc of REAL , the carrier of S, seq be Real_Sequence;

      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 FUNCT_2: 4;

        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;

      now

        let n be Element of NAT ;

        

        thus (( - (h /* seq)) . n) = ( - ((h /* seq) . n)) by BHSP_1: 44

        .= (( - 1) * ((h /* seq) . n)) by RLVECT_1: 16

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

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

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

      end;

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

    end;

    begin

    definition

      let S, f, x0;

      :: NFCONT_3:def1

      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_3:6

    

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

      

       A3: x0 in ( dom f) by A2;

      

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

      hence

       A5: x0 in ( dom (f | X)) by A1, A3, XBOOLE_0:def 4;

      let s1 such that

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

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

      

       A8: ( rng s1) c= ( dom f) by A6, A4, XBOOLE_1: 18;

      

       A9: ((f | X) /* s1) = (f /* s1) by A6, FUNCT_2: 117;

      hence ((f | X) /* s1) is convergent by A2, A7, A8;

      x0 in REAL by XREAL_0:def 1;

      

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

      .= ( lim ((f | X) /* s1)) by A2, A7, A8, A9;

    end;

    theorem :: NFCONT_3:7

    f is_continuous_in x0 iff x0 in ( dom f) & for s1 st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 & (for n holds (s1 . n) <> x0) holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1))

    proof

      thus f is_continuous_in x0 implies x0 in ( dom f) & for s1 st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 & (for n holds (s1 . n) <> x0) holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1));

      assume

       A1: x0 in ( dom f) & for s1 st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 & (for n holds (s1 . n) <> x0) holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1));

      thus x0 in ( dom f) by A1;

      let s2 such that

       A2: ( rng s2) c= ( dom f) and

       A3: s2 is convergent & ( lim s2) = x0;

      per cases ;

        suppose ex n st for m st n <= m holds (s2 . m) = x0;

        then

        consider N be Nat such that

         A4: for m st N <= m holds (s2 . m) = x0;

        

         A5: (f /* (s2 ^\ N)) = ((f /* s2) ^\ N) by A2, VALUED_0: 27;

         A6:

        now

          let p be Real such that

           A7: p > 0 ;

          reconsider n = 0 as Nat;

          take n;

          let m such that n <= m;

          

           A8: (s2 . (m + N)) = x0 by A4, NAT_1: 12;

          

           A9: m in NAT by ORDINAL1:def 12;

          ( rng (s2 ^\ N)) c= ( rng s2) by VALUED_0: 21;

          

          then ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| = ||.((f /. ((s2 ^\ N) . m)) - (f /. x0)).|| by A2, FUNCT_2: 109, XBOOLE_1: 1, A9

          .= ||.((f /. x0) - (f /. x0)).|| by A8, NAT_1:def 3

          .= 0 by NORMSP_1: 6;

          hence ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p by A7;

        end;

        then

         A10: (f /* (s2 ^\ N)) is convergent by NORMSP_1:def 6;

        then (f /. x0) = ( lim ((f /* s2) ^\ N)) by A6, A5, NORMSP_1:def 7;

        hence thesis by A10, A5, LOPBAN_3: 10, LOPBAN_3: 11;

      end;

        suppose

         A11: for n holds ex m st n <= m & (s2 . m) <> x0;

        defpred P[ Nat, set, set] means for n, m st $2 = n & $3 = m holds n < m & (s2 . m) <> x0 & (for k st n < k & (s2 . k) <> x0 holds m <= k);

        defpred P[ set] means (s2 . $1) <> x0;

        ex m1 be Nat st 0 <= m1 & (s2 . m1) <> x0 by A11;

        then

         A12: ex m be Nat st P[m];

        consider M be Nat such that

         A13: P[M] & for n be Nat st P[n] holds M <= n from NAT_1:sch 5( A12);

        reconsider M9 = M as Element of NAT by ORDINAL1:def 12;

         A14:

        now

          let n;

          consider m such that

           A15: (n + 1) <= m & (s2 . m) <> x0 by A11;

          take m;

          thus n < m & (s2 . m) <> x0 by A15, NAT_1: 13;

        end;

        

         A16: for n be Nat, x be Element of NAT holds ex y be Element of NAT st P[n, x, y]

        proof

          let n be Nat, x be Element of NAT ;

          defpred P[ Nat] means x < $1 & (s2 . $1) <> x0;

          ex m st P[m] by A14;

          then

           A17: ex m be Nat st P[m];

          consider l be Nat such that

           A18: P[l] & for k be Nat st P[k] holds l <= k from NAT_1:sch 5( A17);

          take l;

          l in NAT by ORDINAL1:def 12;

          hence thesis by A18;

        end;

        consider F be sequence of NAT such that

         A19: (F . 0 ) = M9 & for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A16);

        ( dom F) = NAT & ( rng F) c= REAL by FUNCT_2:def 1, XBOOLE_1: 1, NUMBERS: 19;

        then

        reconsider F as Real_Sequence by RELSET_1: 4;

        for n holds (F . n) < (F . (n + 1)) by A19;

        then

        reconsider F as increasing sequence of NAT by SEQM_3:def 6;

        

         A20: for n st (s2 . n) <> x0 holds ex m st (F . m) = n

        proof

          defpred P[ set] means (s2 . $1) <> x0 & for m holds (F . m) <> $1;

          assume ex n st P[n];

          then

           A21: ex n be Nat st P[n];

          consider M1 be Nat such that

           A22: P[M1] & for n be Nat st P[n] holds M1 <= n from NAT_1:sch 5( A21);

          reconsider M1 as Nat;

          defpred P[ Nat] means $1 < M1 & (s2 . $1) <> x0 & ex m st (F . m) = $1;

          

           A23: ex n be Nat st P[n]

          proof

            take M;

            M <= M1 & M <> M1 by A13, A19, A22;

            hence M < M1 by XXREAL_0: 1;

            thus (s2 . M) <> x0 by A13;

            take 0 ;

            thus thesis by A19;

          end;

          

           A24: for n be Nat st P[n] holds n <= M1;

          consider MX be Nat such that

           A25: P[MX] & for n be Nat st P[n] holds n <= MX from NAT_1:sch 6( A24, A23);

          consider m such that

           A26: (F . m) = MX by A25;

          

           A27: MX < (F . (m + 1)) & (s2 . (F . (m + 1))) <> x0 by A19, A26;

          (F . (m + 1)) <> M1 & (F . (m + 1)) <= M1 by A19, A22, A25, A26;

          then (F . (m + 1)) < M1 by XXREAL_0: 1;

          hence contradiction by A25, A27;

        end;

        

         A28: for n holds ((s2 * F) . n) <> x0

        proof

          defpred P[ Nat] means ((s2 * F) . $1) <> x0;

          

           A29: for k st P[k] holds P[(k + 1)]

          proof

            let k such that ((s2 * F) . k) <> x0;

            reconsider k as Element of NAT by ORDINAL1:def 12;

            (F . k) in NAT & (F . (k + 1)) in NAT ;

            then (s2 . (F . (k + 1))) <> x0 by A19;

            hence thesis by FUNCT_2: 15;

          end;

          

           A30: P[ 0 ] by A13, A19, FUNCT_2: 15;

          thus for n holds P[n] from NAT_1:sch 2( A30, A29);

        end;

        

         A31: (s2 * F) is convergent & ( lim (s2 * F)) = x0 by A3, SEQ_4: 16, SEQ_4: 17;

        

         A32: ( rng (s2 * F)) c= ( rng s2) by VALUED_0: 21;

        then ( rng (s2 * F)) c= ( dom f) by A2, XBOOLE_1: 1;

        then

         A33: (f /* (s2 * F)) is convergent & (f /. x0) = ( lim (f /* (s2 * F))) by A1, A28, A31;

         A34:

        now

          let p be Real;

          assume

           A35: 0 < p;

          then

          consider n such that

           A36: for m st n <= m holds ||.(((f /* (s2 * F)) . m) - (f /. x0)).|| < p by A33, NORMSP_1:def 7;

          reconsider k = (F . n) as Nat;

          take k;

          let m such that

           A37: k <= m;

          

           A38: m in NAT by ORDINAL1:def 12;

          per cases ;

            suppose (s2 . m) = x0;

            

            then ||.(((f /* s2) . m) - (f /. x0)).|| = ||.((f /. x0) - (f /. x0)).|| by A2, FUNCT_2: 109, A38

            .= 0 by NORMSP_1: 6;

            hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A35;

          end;

            suppose (s2 . m) <> x0;

            then

            consider l be Nat such that

             A39: m = (F . l) by A20;

            

             A40: l in NAT by ORDINAL1:def 12;

            n <= l by A37, A39, SEQM_3: 1;

            then ||.(((f /* (s2 * F)) . l) - (f /. x0)).|| < p by A36;

            then ||.((f /. ((s2 * F) . l)) - (f /. x0)).|| < p by A2, A32, FUNCT_2: 109, XBOOLE_1: 1, A40;

            then ||.((f /. (s2 . m)) - (f /. x0)).|| < p by A39, FUNCT_2: 15, A40;

            hence ||.(((f /* s2) . m) - (f /. x0)).|| < p by A2, FUNCT_2: 109, A38;

          end;

        end;

        hence (f /* s2) is convergent by NORMSP_1:def 6;

        hence (f /. x0) = ( lim (f /* s2)) by A34, NORMSP_1:def 7;

      end;

    end;

    theorem :: NFCONT_3:8

    

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

        defpred P[ Nat, Real] 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 Element of REAL 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 x1 such that

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

          take x1;

          thus thesis by A5;

        end;

        consider s1 such that

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

        now

          let x be object;

          assume x in ( rng s1);

          then ex n be Element of NAT st x = (s1 . n) by FUNCT_2: 113;

          hence x in ( dom f) by A6;

        end;

        then

         A7: ( rng s1) c= ( dom f) by TARSKI:def 3;

         A8:

        now

          let s be Real;

          assume

           A9: 0 < s;

          consider n such that

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

          ((s " ) + 0 qua Nat) < (n + 1) by A10, XREAL_1: 8;

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

          then

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

          take k = n;

          let m;

          

           A12: 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 A11, XXREAL_0: 2;

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

        end;

        then

         A13: s1 is convergent by SEQ_2:def 6;

        then ( lim s1) = x0 by A8, SEQ_2:def 7;

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

        then

        consider n such that

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

        

         A15: n in NAT by ORDINAL1:def 12;

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

        then ||.((f /. (s1 . n)) - (f /. x0)).|| < r by A7, FUNCT_2: 109, A15;

        hence contradiction by A6, A15;

      end;

      assume

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

      now

        let s1 such that

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

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

         A19:

        now

          let p be Real;

          assume 0 < p;

          then

          consider s such that

           A20: 0 < s and

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

          consider n such that

           A22: for m st n <= m holds |.((s1 . m) - x0).| < s by A18, A20, SEQ_2:def 7;

          take k = n;

          let m;

          

           A23: m in NAT by ORDINAL1:def 12;

          assume k <= m;

          then (s1 . m) in ( rng s1) & |.((s1 . m) - x0).| < s by A22, VALUED_0: 28;

          then ||.((f /. (s1 . m)) - (f /. x0)).|| < p by A17, A21;

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

        end;

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

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

      end;

      hence thesis by A16;

    end;

    theorem :: NFCONT_3:9

    

     Th9: for S, 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 S, 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 N01 be Neighbourhood of (f /. x0);

        consider r such that

         A2: 0 < r and

         A3: { p where p be Point of S : ||.(p - (f /. x0)).|| < r } c= N01 by NFCONT_1:def 1;

        set N1 = { p where p be Point of S : ||.(p - (f /. x0)).|| < r };

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

        reconsider N = ].(x0 - s), (x0 + s).[ as Neighbourhood of x0 by A4, RCOMP_1:def 6;

        take N;

        let x1;

        assume that

         A6: x1 in ( dom f) and

         A7: x1 in N;

         |.(x1 - x0).| < s by A7, RCOMP_1: 1;

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

        then (f /. x1) in N1;

        hence thesis by A3;

      end;

      assume

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

      now

        let r;

        assume 0 < r;

        then

        reconsider N1 = { p where p be Point of S : ||.(p - (f /. x0)).|| < r } as Neighbourhood of (f /. x0) by NFCONT_1: 3;

        consider N2 be Neighbourhood of x0 such that

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

        consider s be Real such that

         A10: 0 < s and

         A11: N2 = ].(x0 - s), (x0 + s).[ by RCOMP_1:def 6;

        take s;

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

        proof

          let x1;

          assume that

           A12: x1 in ( dom f) and

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

          x1 in N2 by A11, A13, RCOMP_1: 1;

          then (f /. x1) in N1 by A9, A12;

          then ex p be Point of S st p = (f /. x1) & ||.(p - (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 A10;

      end;

      hence thesis by A8, Th8;

    end;

    theorem :: NFCONT_3:10

    

     Th10: for S, 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 S, 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 Element of REAL such that

           A3: x in ( dom f) & x in N & r = (f . x) by PARTFUN2: 59;

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

          hence r in N1 by A2, A3;

        end;

        hence thesis by TARSKI:def 3;

      end;

      assume

       A4: x0 in ( dom f) & 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

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

        take N;

        let x1;

        assume

         A6: x1 in ( dom f) & x1 in N;

        then (f . x1) in (f .: N) by FUNCT_1:def 6;

        then (f /. x1) in (f .: N) by A6, PARTFUN1:def 6;

        hence (f /. x1) in N1 by A5;

      end;

      hence thesis by A4, Th9;

    end;

    theorem :: NFCONT_3:11

    (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};

      x0 in (( dom f) /\ N) by A1, TARSKI:def 1;

      then

       A2: x0 in ( dom f) by XBOOLE_0:def 4;

      now

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

        take N;

        

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

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

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

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

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

      end;

      hence thesis by Th10, A2;

    end;

    theorem :: NFCONT_3:12

    x0 in (( dom f1) /\ ( dom f2)) & 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

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

      assume that

       A2: f1 is_continuous_in x0 & f2 is_continuous_in x0;

      

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

      

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

      now

        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)) c= ( dom f1) & ( dom (f1 + f2)) c= ( dom f2) by A3, XBOOLE_1: 17;

        then

         A8: ( rng s1) c= ( dom f1) & ( rng s1) c= ( dom f2) by A5, XBOOLE_1: 1;

        then

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

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

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

        

         A10: (f1 /. x0) = ( lim (f1 /* s1)) & (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 A9, A10, NORMSP_1: 25

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

      end;

      hence (f1 + f2) is_continuous_in x0 by A4;

      

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

      

       A12: x0 in ( dom (f1 - f2)) by A1, VFUNCT_1:def 2;

      now

        let s1;

        assume that

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

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

        

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

        ( dom (f1 - f2)) c= ( dom f1) & ( dom (f1 - f2)) c= ( dom f2) by A11, XBOOLE_1: 17;

        then

         A16: ( rng s1) c= ( dom f1) & ( rng s1) c= ( dom f2) by A13, XBOOLE_1: 1;

        then

         A17: (f1 /* s1) is convergent & (f2 /* s1) is convergent by A2, A14;

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

        hence ((f1 - f2) /* s1) is convergent by A15, Th2;

        

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

        

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

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

        .= ( lim ((f1 - f2) /* s1)) by A15, Th2;

      end;

      hence (f1 - f2) is_continuous_in x0 by A12;

    end;

    theorem :: NFCONT_3:13

    

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

      

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

      

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

    end;

    theorem :: NFCONT_3:14

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

    proof

      assume

       A1: x0 in ( dom f);

      assume

       A2: f is_continuous_in x0;

      

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

      now

        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 A2, A5;

        

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

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

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

        

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

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

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

      end;

      hence ||.f.|| is_continuous_in x0;

      (( - 1) (#) f) is_continuous_in x0 by A2, Th13;

      hence thesis by VFUNCT_1: 23;

    end;

    theorem :: NFCONT_3:15

    for f1 be PartFunc of REAL , the carrier of S, f2 be PartFunc of the carrier of S, the carrier of T 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 , the carrier of S, f2 be PartFunc of the carrier of S, the carrier of T;

      assume

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

      assume that

       A2: f1 is_continuous_in x0 and

       A3: f2 is_continuous_in (f1 /. x0);

      thus x0 in ( dom (f2 * f1)) by A1;

      let s1 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;

      now

        let x be object;

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

        then

        consider n be Element of NAT such that

         A7: 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, A7, FUNCT_2: 108, XBOOLE_1: 1;

      end;

      then

       A8: ( rng (f1 /* s1)) c= ( dom f2) by TARSKI:def 3;

       A9:

      now

        let n be Element of NAT ;

        (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 A8, FUNCT_2: 108;

      end;

      then

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

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

      then

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

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

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

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

      hence thesis by A3, A12, A8, A11, NFCONT_1:def 5;

    end;

    definition

      let S, f;

      :: NFCONT_3:def2

      attr f is continuous means

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

    end

    theorem :: NFCONT_3:16

    

     Th16: for X, f st X c= ( dom f) holds (f | X) is continuous iff 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 such that

       A1: X c= ( dom f);

      thus (f | X) is continuous implies 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

         A2: (f | X) is continuous;

        hereby

          let s1 such that

           A3: ( rng s1) c= X and

           A4: s1 is convergent and

           A5: ( lim s1) in X;

          

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

          .= X by A1, XBOOLE_1: 28;

          then

           A7: (f | X) is_continuous_in ( lim s1) by A2, A5;

          now

            let n be Element of NAT ;

            

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

            

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

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

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

          end;

          then

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

          ( lim s1) in REAL by XREAL_0:def 1;

          

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

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

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

        end;

      end;

      assume

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

        

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

        .= X by A1, XBOOLE_1: 28;

        let x1 such that

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

        now

          let s1 such that

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

           A14: s1 is convergent and

           A15: ( lim s1) = x1;

          now

            let n be Element of NAT ;

            

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

            

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

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

            .= ((f /* s1) . n) by A1, A11, A13, FUNCT_2: 109, XBOOLE_1: 1;

          end;

          then

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

          ( lim s1) in REAL by XREAL_0:def 1;

          

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

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

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

        end;

        hence (f | X) is_continuous_in x1 by A12;

      end;

      hence thesis;

    end;

    theorem :: NFCONT_3:17

    

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

        take s;

        thus 0 < s by A5;

        let x1;

        assume that

         A7: x1 in X and

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

        

         A9: x0 in REAL by XREAL_0:def 1;

        

         A10: x1 in REAL by XREAL_0:def 1;

        

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

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

        hence thesis by A6, A11, A7, A8;

      end;

      assume

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

      now

        let x0;

        assume

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

        then

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

           A15: 0 < s and

           A16: for x1 st x1 in X & |.(x1 - x0).| < s holds ||.((f /. x1) - (f /. x0)).|| < r by A12, A14;

          take s;

          thus 0 < s by A15;

          let x1 such that

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

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

          

           A19: x0 in REAL by XREAL_0:def 1;

          

           A20: x1 in REAL by XREAL_0:def 1;

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

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

          hence thesis by A16, A17, A18;

        end;

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

      end;

      hence thesis;

    end;

    registration

      let S;

      cluster constant -> continuous for PartFunc of REAL , the carrier of S;

      coherence

      proof

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

        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, NORMSP_1: 6;

        end;

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

        hence thesis;

      end;

    end

    registration

      let S;

      cluster continuous for PartFunc of REAL , the carrier of S;

      existence

      proof

        set f = the constant PartFunc of REAL , the carrier of S;

        take f;

        thus thesis;

      end;

    end

    registration

      let S;

      let f be continuous PartFunc of REAL , the carrier of S, X be set;

      cluster (f | X) -> continuous;

      coherence

      proof

        now

          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 Def2;

          x0 in X by A1;

          hence (f | X) is_continuous_in x0 by A2, Th6;

        end;

        hence thesis;

      end;

    end

    theorem :: NFCONT_3:18

    

     Th18: (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 S;

      cluster empty -> continuous for PartFunc of REAL , the carrier of S;

      coherence ;

    end

    registration

      let S, f;

      let X be trivial set;

      cluster (f | X) -> continuous;

      coherence

      proof

        now

          assume not (f | X) is empty;

          then

          consider x0 such that

           A1: x0 in ( dom (f | X) qua PartFunc of REAL , the carrier of S) by MEMBERED: 9;

          x0 in X by A1, RELAT_1: 57;

          then

           A2: X = {x0} by ZFMISC_1: 132;

          now

            let p be Real;

            assume

             A3: p in ( dom (f | X));

            then

             A4: p in {x0} by A2;

            thus (f | X) is_continuous_in p

            proof

              thus p in ( dom (f | X)) by A3;

              let s1;

              assume that

               A5: ( rng s1) c= ( dom (f | X)) and s1 is convergent and ( lim s1) = p;

              

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

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

              then

               A7: ( rng s1) c= {x0} by A6, XBOOLE_1: 1;

               A8:

              now

                let n;

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

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

              end;

              

               A9: p = x0 by A4, TARSKI:def 1;

               A10:

              now

                let g be Real such that

                 A11: 0 < g;

                reconsider n = 0 as Nat;

                take n;

                let m such that n <= m;

                

                 A12: m in NAT by ORDINAL1:def 12;

                 ||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| = ||.(((f | {x0}) /. (s1 . m)) - ((f | {x0}) /. x0)).|| by A2, A9, A5, FUNCT_2: 109, A12

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

                .= 0 by NORMSP_1: 6;

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

              end;

              hence ((f | X) /* s1) is convergent by A2, NORMSP_1:def 6;

              hence ( lim ((f | X) /* s1)) = ((f | X) /. p) by A2, A10, NORMSP_1:def 7;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let S;

      let f1,f2 be continuous PartFunc of REAL , the carrier of S;

      cluster (f1 + f2) -> continuous;

      coherence

      proof

        set X = ( dom (f1 + f2));

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

        then

         A1: X c= ( dom f1) & X c= ( dom f2) by XBOOLE_1: 18;

        

         A2: (f1 | X) is continuous & (f2 | X) is continuous;

        now

          let s1;

          assume that

           A3: ( rng s1) c= X and

           A4: s1 is convergent and

           A5: ( lim s1) in X;

          

           A6: (f1 /* s1) is convergent & (f2 /* s1) is convergent by A1, A2, A3, A4, A5, Th16;

          then

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

          

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

          (f1 /. ( lim s1)) = ( lim (f1 /* s1)) & (f2 /. ( lim s1)) = ( lim (f2 /* s1)) by A1, A2, A3, A4, A5, Th16;

          

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

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

          .= ( lim ((f1 + f2) /* s1)) by A8, Th2;

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

        end;

        then ((f1 + f2) | X) is continuous by Th16;

        hence thesis;

      end;

      cluster (f1 - f2) -> continuous;

      coherence

      proof

        set X = ( dom (f1 - f2));

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

        then

         A9: X c= ( dom f1) & X c= ( dom f2) by XBOOLE_1: 18;

        

         A10: (f1 | X) is continuous & (f2 | X) is continuous;

        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 A9, A10, A11, A12, A13, Th16;

          then

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

          

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

          (f1 /. ( lim s1)) = ( lim (f1 /* s1)) & (f2 /. ( lim s1)) = ( lim (f2 /* s1)) by A9, A10, A11, A12, A13, Th16;

          

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

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

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

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

        end;

        then ((f1 - f2) | X) is continuous by Th16;

        hence thesis;

      end;

    end

    theorem :: NFCONT_3:19

    

     Th19: for X, f1, f2 st X c= (( dom f1) /\ ( dom f2)) & (f1 | X) is continuous & (f2 | X) is continuous holds ((f1 + f2) | X) is continuous & ((f1 - f2) | X) is continuous

    proof

      let X, f1, f2;

      assume that

       A1: X c= (( dom f1) /\ ( dom f2)) and

       A2: (f1 | X) is continuous & (f2 | X) is continuous;

      

       A3: X c= ( dom f1) & X c= ( dom f2) by A1, XBOOLE_1: 18;

      

       A4: X c= ( dom (f1 + f2)) & X c= ( dom (f1 - f2)) by A1, VFUNCT_1:def 1, VFUNCT_1:def 2;

      now

        let s1;

        assume that

         A5: ( rng s1) c= X & s1 is convergent and

         A6: ( lim s1) in X;

        

         A7: (f1 /* s1) is convergent & (f2 /* s1) is convergent by A3, A2, A5, A6, Th16;

        then

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

        

         A9: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A1, A5, XBOOLE_1: 1;

        

         A10: ( lim s1) in REAL by XREAL_0:def 1;

        (f1 /. ( lim s1)) = ( lim (f1 /* s1)) & (f2 /. ( lim s1)) = ( lim (f2 /* s1)) by A3, A2, A5, A6, Th16;

        

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

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

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

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

      end;

      hence ((f1 + f2) | X) is continuous by A4, Th16;

      now

        let s1;

        assume that

         A11: ( rng s1) c= X & s1 is convergent and

         A12: ( lim s1) in X;

        

         A13: (f1 /* s1) is convergent & (f2 /* s1) is convergent by A3, A2, A11, A12, Th16;

        then

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

        

         A15: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A1, A11, XBOOLE_1: 1;

        

         A16: ( lim s1) in REAL by XREAL_0:def 1;

        (f1 /. ( lim s1)) = ( lim (f1 /* s1)) & (f2 /. ( lim s1)) = ( lim (f2 /* s1)) by A3, A2, A11, A12, Th16;

        

        then ((f1 - f2) /. ( lim s1)) = (( lim (f1 /* s1)) - ( lim (f2 /* s1))) by A4, A12, VFUNCT_1:def 2, A16

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

        .= ( lim ((f1 - f2) /* s1)) by A15, Th2;

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

      end;

      hence ((f1 - f2) | X) is continuous by A4, Th16;

    end;

    theorem :: NFCONT_3:20

    for X, X1, f1, f2 st X c= ( dom f1) & X1 c= ( dom f2) & (f1 | X) is continuous & (f2 | X1) is continuous holds ((f1 + f2) | (X /\ X1)) is continuous & ((f1 - f2) | (X /\ X1)) is continuous

    proof

      let X, X1, f1, f2;

      assume X c= ( dom f1) & X1 c= ( dom f2);

      then

       A1: (X /\ X1) c= (( dom f1) /\ ( dom f2)) by XBOOLE_1: 27;

      assume (f1 | X) is continuous & (f2 | X1) is continuous;

      then (f1 | (X /\ X1)) is continuous & (f2 | (X /\ X1)) is continuous by Th18, XBOOLE_1: 17;

      hence thesis by A1, Th19;

    end;

    registration

      let S;

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

      let r;

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

      coherence

      proof

        set X = ( dom f);

        

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

        then

         A2: ((r (#) f) | X) = (r (#) f);

        now

          let s1;

          assume that

           A3: ( rng s1) c= X and

           A4: s1 is convergent and

           A5: ( lim s1) in X;

          (f | X) is continuous;

          then

           A6: (f /* s1) is convergent & (f /. ( lim s1)) = ( lim (f /* s1)) by A3, A4, A5, Th16;

          then

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

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

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

          .= ( lim ((r (#) f) /* s1)) by A3, Th4;

          hence ((r (#) f) /* s1) is convergent & ((r (#) f) /. ( lim s1)) = ( lim ((r (#) f) /* s1)) by A3, A7, Th4;

        end;

        hence thesis by A1, A2, Th16;

      end;

    end

    theorem :: NFCONT_3:21

    

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

    proof

      assume that

       A1: X c= ( dom f) and

       A2: (f | X) is continuous;

      

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

      now

        let s1;

        assume that

         A4: ( rng s1) c= X & s1 is convergent and

         A5: ( lim s1) in X;

        

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

        then

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

        

         A8: ( lim s1) in REAL by XREAL_0:def 1;

        (f /. ( lim s1)) = ( lim (f /* s1)) by A1, A2, A4, A5, Th16;

        

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

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

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

        hence ((r (#) f) /* s1) is convergent & ((r (#) f) /. ( lim s1)) = ( lim ((r (#) f) /* s1)) by A1, A4, A7, Th4, XBOOLE_1: 1;

      end;

      hence thesis by A3, Th16;

    end;

    theorem :: NFCONT_3:22

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

    proof

      assume that

       A1: X c= ( dom f) and

       A2: (f | X) is continuous;

      thus ( ||.f.|| | X) is continuous

      proof

        let r be Real;

        assume

         A3: r in ( dom ( ||.f.|| | X));

        then

         A4: r in ( dom ||.f.||) & r in X by RELAT_1: 57;

        then r in ( dom f) by NORMSP_0:def 3;

        then

         A5: r in ( dom (f | X)) by A4, RELAT_1: 57;

        then

         A6: (f | X) is_continuous_in r by A2;

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

        proof

          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;

          now

            let n be Element of NAT ;

            

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

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

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

            then

             A11: (s1 . n) in X & (s1 . n) in ( dom f) by XBOOLE_0:def 4;

            then

             A12: (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, A10, PARTFUN2: 15

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

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

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

          end;

          then

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

          r in REAL by XREAL_0:def 1;

          

          then

           A14: ||.((f | X) /. r).|| = ||.(f /. r).|| by A5, PARTFUN2: 15

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

          .= (( ||.f.|| | X) . r) by A3, FUNCT_1: 47;

          

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

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

          ((f | X) /. r) = ( lim ((f | X) /* s1)) by A6, A8, A9;

          hence thesis by A15, A13, A14, LOPBAN_1: 20;

        end;

      end;

      ((( - 1) (#) f) | X) is continuous by A1, A2, Th21;

      hence thesis by VFUNCT_1: 23;

    end;

    theorem :: NFCONT_3:23

    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 that

       A1: f is total and

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

      

       A3: ( dom f) = REAL by A1, PARTFUN1:def 2;

      given x0 such that

       A4: f is_continuous_in x0;

      reconsider z0 = 0 as Real;

      ((f /. z0) + (f /. z0)) = (f /. (z0 + z0)) by A2;

      then ((f /. z0) + ((f /. z0) - (f /. z0))) = ((f /. z0) - (f /. z0)) by RLVECT_1: 28;

      then ((f /. z0) + ( 0. S)) = ((f /. z0) - (f /. z0)) by RLVECT_1: 15;

      then

       A5: ((f /. z0) + ( 0. S)) = ( 0. S) by RLVECT_1: 15;

       A6:

      now

        let x1;

        ( 0. S) = (f /. (x1 + ( - x1))) by A5, RLVECT_1: 4;

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

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

      end;

       A7:

      now

        let x1, x2;

        (f /. (x1 - x2)) = (f /. (x1 + ( - x2)));

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

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

      end;

      now

        let x1, r;

        assume that x1 in REAL 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, Th8;

        take s;

        thus s > 0 by A9;

        let x2 such that x2 in REAL and

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

        

         A12: (x2 - y) in REAL & |.((x2 - y) - x0).| = |.(x2 - x1).| by XREAL_0:def 1;

        (y + x0) = x1;

        

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

        .= ||.(((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, A12;

      end;

      hence thesis by A3, Th17;

    end;

    theorem :: NFCONT_3:24

    

     Th24: ( dom f) is compact & (f | ( dom f)) is continuous implies ( rng f) is compact

    proof

      assume that

       A1: ( dom f) is compact and

       A2: (f | ( dom f)) is continuous;

      now

        let s1 be sequence of S 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 Element of REAL 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 Element of REAL 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 Real_Sequence 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 ex n be Element of NAT st x = (q1 . n) by FUNCT_2: 113;

          hence x in ( dom f) by A6;

        end;

        then

         A7: ( rng q1) c= ( dom f) by TARSKI:def 3;

        then

        consider s2 such that

         A8: s2 is subsequence of q1 and

         A9: s2 is convergent and

         A10: ( lim s2) in ( dom f) by A1, RCOMP_1:def 3;

        take q2 = (f /* s2);

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

        then

         A11: ( rng s2) c= ( dom f) by A7, XBOOLE_1: 1;

        now

          let n be Element of NAT ;

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

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

        end;

        then

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

        ( lim s2) in ( dom (f | ( dom f))) by A10;

        then (f | ( dom f)) is_continuous_in ( lim s2) by A2;

        then

         A13: f is_continuous_in ( lim s2);

        then (f /. ( lim s2)) = ( lim (f /* s2)) by A9, A11;

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

      end;

      hence thesis by NFCONT_1:def 2;

    end;

    theorem :: NFCONT_3:25

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

    proof

      assume that

       A1: Y c= ( dom f) and

       A2: Y is compact and

       A3: (f | Y) is continuous;

      

       A4: ((f | Y) | Y) is continuous by A3;

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

      .= Y by A1, XBOOLE_1: 28;

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

      hence thesis by RELAT_1: 115;

    end;

    begin

    definition

      let S, f;

      :: NFCONT_3:def3

      attr f is Lipschitzian means

      : Def3: 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).|);

    end

    theorem :: NFCONT_3:26

    

     Th26: (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

      thus (f | X) is Lipschitzian implies 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

        given r be Real such that

         A1: 0 < r and

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

        take r;

        thus 0 < r by A1;

        let x1, x2;

        

         A3: x1 in REAL & x2 in REAL by XREAL_0:def 1;

        assume

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

        then ((f | X) /. x1) = (f /. x1) & ((f | X) /. x2) = (f /. x2) by A3, PARTFUN2: 15;

        hence thesis by A2, A4;

      end;

      given r be Real such that

       A5: 0 < r and

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

      take r;

      thus 0 < r by A5;

      let x1, x2;

      

       A7: x1 in REAL & x2 in REAL by XREAL_0:def 1;

      assume

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

      then ((f | X) /. x1) = (f /. x1) & ((f | X) /. x2) = (f /. x2) by A7, PARTFUN2: 15;

      hence thesis by A6, A8;

    end;

    registration

      let S;

      cluster empty -> Lipschitzian for PartFunc of REAL , the carrier of S;

      coherence

      proof

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

        assume

         A1: f is empty;

        take 1;

        thus thesis by A1;

      end;

    end

    registration

      let S;

      cluster empty for PartFunc of REAL , the carrier of S;

      existence

      proof

        take the empty PartFunc of REAL , the carrier of S;

        thus thesis;

      end;

    end

    registration

      let S;

      let f be Lipschitzian PartFunc of REAL , the carrier of S, X be set;

      cluster (f | X) -> Lipschitzian;

      coherence

      proof

        consider r be Real such that

         A1: 0 < r and

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

        now

          let x1, x2;

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

          then x1 in ( dom f) & x2 in ( dom f) by RELAT_1: 57;

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

        end;

        hence thesis by A1, Th26;

      end;

    end

    theorem :: NFCONT_3:27

    (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 S;

      let f1,f2 be Lipschitzian PartFunc of REAL , the carrier of S;

      cluster (f1 + f2) -> Lipschitzian;

      coherence

      proof

        set X = ( dom f1), X1 = ( dom f2);

        consider s such that

         A1: 0 < s and

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

        consider g such that

         A3: 0 < g and

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

        now

          take p = (s + g);

          thus 0 < p by A1, A3;

          let x1, x2;

          assume

           A5: x1 in ( dom (f1 + f2)) & x2 in ( dom (f1 + f2));

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

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

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

          .= ||.((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: 28

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

          then

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

          ( dom (f2 | (X /\ X1))) = (( dom f2) /\ (X /\ X1)) by RELAT_1: 61

          .= ((( dom f2) /\ X1) /\ X) by XBOOLE_1: 16

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

          then

           A7: ||.((f2 /. x1) - (f2 /. x2)).|| <= (g * |.(x1 - x2).|) by A4, A5;

          ( dom (f1 | (X /\ X1))) = (( dom f1) /\ (X /\ X1)) by RELAT_1: 61

          .= ((( dom f1) /\ X) /\ X1) by XBOOLE_1: 16

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

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

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

          hence ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= (p * |.(x1 - x2).|) by A6, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      cluster (f1 - f2) -> Lipschitzian;

      coherence

      proof

        set X = ( dom f1), X1 = ( dom f2);

        consider s such that

         A8: 0 < s and

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

        consider g be Real such that

         A10: 0 < g and

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

        now

          take p = (s + g);

          thus 0 < p by A8, A10;

          let x1, x2;

          assume

           A12: x1 in ( dom (f1 - f2)) & x2 in ( dom (f1 - f2));

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

          .= ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).|| by 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: 28

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

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

          then

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

          ( dom (f2 | (X /\ X1))) = (( dom f2) /\ (X /\ X1)) by RELAT_1: 61

          .= ((( dom f2) /\ X1) /\ X) by XBOOLE_1: 16

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

          then

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

          ( dom (f1 | (X /\ X1))) = (( dom f1) /\ (X /\ X1)) by RELAT_1: 61

          .= ((( dom f1) /\ X) /\ X1) by XBOOLE_1: 16

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

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

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

          hence ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= (p * |.(x1 - x2).|) by A13, XXREAL_0: 2;

        end;

        hence thesis;

      end;

    end

    theorem :: NFCONT_3:28

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

    proof

      

       A1: (f1 | (X /\ X1)) = ((f1 | X) | (X /\ X1)) & (f2 | (X /\ X1)) = ((f2 | X1) | (X /\ X1)) by RELAT_1: 74, XBOOLE_1: 17;

      

       A2: ((f1 + f2) | (X /\ X1)) = ((f1 | (X /\ X1)) + (f2 | (X /\ X1))) by VFUNCT_1: 27;

      assume (f1 | X) is Lipschitzian & (f2 | X1) is Lipschitzian;

      hence thesis by A1, A2;

    end;

    theorem :: NFCONT_3:29

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

    proof

      

       A1: (f1 | (X /\ X1)) = ((f1 | X) | (X /\ X1)) & (f2 | (X /\ X1)) = ((f2 | X1) | (X /\ X1)) by RELAT_1: 74, XBOOLE_1: 17;

      

       A2: ((f1 - f2) | (X /\ X1)) = ((f1 | (X /\ X1)) - (f2 | (X /\ X1))) by VFUNCT_1: 30;

      assume (f1 | X) is Lipschitzian & (f2 | X1) is Lipschitzian;

      hence thesis by A1, A2;

    end;

    registration

      let S;

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

      let p;

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

      coherence

      proof

        consider s such that

         A1: 0 < s and

         A2: for x1, x2 st x1 in ( dom f) & x2 in ( dom f) holds ||.((f /. x1) - (f /. x2)).|| <= (s * |.(x1 - x2).|) by Def3;

        per cases ;

          suppose

           A3: p = 0 ;

          now

            take s;

            thus 0 < s by A1;

            let x1, x2;

            assume

             A4: x1 in ( dom (p (#) f)) & x2 in ( dom (p (#) f));

            

             A5: 0 <= |.(x1 - x2).| by COMPLEX1: 46;

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

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

            .= ||.(( 0. S) - (p * (f /. x2))).|| by A3, RLVECT_1: 10

            .= ||.(( 0. S) - ( 0. S)).|| by A3, RLVECT_1: 10

            .= 0 by NORMSP_1: 6;

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

          end;

          hence thesis;

        end;

          suppose p <> 0 ;

          then 0 < |.p.| by COMPLEX1: 47;

          then

           A6: ( 0 * s) < ( |.p.| * s) by A1, XREAL_1: 68;

          now

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

            

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

            thus 0 < g by A6;

            let x1, x2;

            assume

             A8: x1 in ( dom (p (#) f)) & x2 in ( dom (p (#) f));

            

            then

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

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

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

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

            x1 in ( dom f) & x2 in ( dom f) by A8, VFUNCT_1:def 4;

            then ( |.p.| * ||.((f /. x1) - (f /. x2)).||) <= ( |.p.| * (s * |.(x1 - x2).|)) by A2, A7, XREAL_1: 64;

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

          end;

          hence thesis;

        end;

      end;

    end

    theorem :: NFCONT_3:30

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

    proof

      ((p (#) f) | X) = (p (#) (f | X)) by VFUNCT_1: 31;

      hence thesis;

    end;

    registration

      let S;

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

      cluster ||.f.|| -> Lipschitzian;

      coherence

      proof

        consider s such that

         A1: 0 < s and

         A2: for x1, x2 st x1 in ( dom f) & x2 in ( dom f) holds ||.((f /. x1) - (f /. x2)).|| <= (s * |.(x1 - x2).|) by Def3;

        now

          let x1, x2;

          assume

           A3: x1 in ( dom ||.f.||) & x2 in ( dom ||.f.||);

          then x1 in ( dom f) & x2 in ( dom f) by NORMSP_0:def 3;

          then

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

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

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

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

          hence |.(( ||.f.|| . x1) - ( ||.f.|| . x2)).| <= (s * |.(x1 - x2).|) by A4, XXREAL_0: 2;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: NFCONT_3:31

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

    proof

      assume

       A1: (f | X) is Lipschitzian;

      

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

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

      thus (( - f) | X) is Lipschitzian by A1, A2, VFUNCT_1: 29;

      ( ||.f.|| | X) = ||.(f | X).|| by VFUNCT_1: 29;

      hence thesis by A1;

    end;

    registration

      let S;

      cluster constant -> Lipschitzian for PartFunc of REAL , the carrier of S;

      coherence

      proof

        let f be PartFunc of REAL , the carrier of S such that

         A1: f is constant;

        now

          let x1, x2;

          assume

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

          

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

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

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

          then ||.((f /. x1) - (f /. x2)).|| = 0 by NORMSP_1: 6;

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

        end;

        hence thesis;

      end;

    end

    registration

      let S;

      cluster Lipschitzian -> continuous for PartFunc of REAL , the carrier of S;

      coherence

      proof

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

        set X = ( dom f);

        assume f is Lipschitzian;

        then

        consider r be Real such that

         A1: 0 < r and

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

        now

          let x0 such that

           A3: x0 in X;

          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 g be Real such that

             A4: 0 < g;

            set s = (g / r);

            take s9 = s;

             A5:

            now

              let x1;

              assume that

               A6: x1 in ( dom f) and

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

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

              then

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

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

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

            end;

            s9 = (g * (r " )) by XCMPLX_0:def 9;

            hence thesis by A1, A4, A5, XREAL_1: 129;

          end;

          hence f is_continuous_in x0 by A3, Th8;

        end;

        hence thesis;

      end;

    end

    theorem :: NFCONT_3:32

    (ex r be Point of S st ( rng f) = {r}) implies f is continuous

    proof

      given r be Point of S such that

       A1: ( rng f) = {r};

      now

        let x1, x2;

        assume

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

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

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

        then

         A3: (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 by A3, NORMSP_1: 6;

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

      end;

      then f is Lipschitzian;

      hence thesis;

    end;

    theorem :: NFCONT_3:33

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

    proof

      let r,p be Point of S;

      assume

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

       A2:

      now

        let x1, x2;

        assume

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

        then x2 in X;

        then

         A4: (f /. x2) = ((x2 * r) + p) by A1;

        

         A5: 0 <= |.(x1 - x2).| by COMPLEX1: 46;

        x1 in X by A3;

        then (f /. x1) = ((x1 * r) + p) by A1;

        

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

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

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

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

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

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

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

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

      end;

      ( 0 qua Nat + 0 qua Nat) < ( ||.r.|| + 1) by NORMSP_1: 4, XREAL_1: 8;

      then (f | X) is Lipschitzian by A2, Th26;

      hence thesis;

    end;