fcont_1.miz



    begin

    reserve n,m,k for Element of NAT ;

    reserve x,X,X1,Z,Z1 for set;

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

    reserve s1,s2,q1 for Real_Sequence;

    reserve Y for Subset of REAL ;

    reserve f,f1,f2 for PartFunc of REAL , REAL ;

    definition

      let f, x0;

      :: FCONT_1:def1

      pred f is_continuous_in x0 means 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 :: FCONT_1:1

    

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

      let s1 such that

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

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

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

      then

       A5: ( rng s1) c= ( dom f) by A3, XBOOLE_1: 18;

      

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

      hence ((f | X) /* s1) is convergent by A2, A4, A5;

      

      thus ((f | X) . x0) = (f . x0) by A1, FUNCT_1: 49

      .= ( lim ((f | X) /* s1)) by A2, A4, A5, A6;

    end;

    theorem :: FCONT_1:2

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

    proof

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

      assume

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

      let s2 such that

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

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

      now

        per cases ;

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

          then

          consider N be Element of NAT such that

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

          

           A5: for n holds ((s2 ^\ N) . n) = x0

          proof

            let n;

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

            hence thesis by NAT_1:def 3;

          end;

          

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

          

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

           A8:

          now

            let p be Real such that

             A9: p > 0 ;

            reconsider zz = 0 as Nat;

            take n = zz;

            let m be Nat such that n <= m;

            

             A10: m in NAT by ORDINAL1:def 12;

            

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

            .= |.((f . x0) - (f . x0)).| by A5, A10

            .= 0 by ABSVALUE: 2;

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

          end;

          then

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

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

          hence thesis by A11, A6, SEQ_4: 20, SEQ_4: 21;

        end;

          suppose

           A12: 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 P1[ set] means (s2 . $1) <> x0;

          ex m1 be Element of NAT st 0 <= m1 & (s2 . m1) <> x0 by A12;

          then

           A13: ex m be Nat st P1[m];

          consider M be Nat such that

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

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

           A15:

          now

            let n;

            consider m such that

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

            take m;

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

          end;

          

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

          proof

            let n be Nat;

            let x be Element of NAT ;

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

            ex m st P2[m] by A15;

            then

             A18: ex m be Nat st P2[m];

            consider l be Nat such that

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

            take l;

            l in NAT by ORDINAL1:def 12;

            hence thesis by A19;

          end;

          consider F be sequence of NAT such that

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

          

           A21: ( rng F) c= REAL by NUMBERS: 19;

          

           A22: ( rng F) c= NAT ;

          

           A23: ( dom F) = NAT by FUNCT_2:def 1;

          then

          reconsider F as Real_Sequence by A21, RELSET_1: 4;

           A24:

          now

            let n;

            (F . n) in ( rng F) by A23, FUNCT_1:def 3;

            hence (F . n) is Element of NAT by A22;

          end;

          now

            let n be Nat;

            n in NAT by ORDINAL1:def 12;

            then (F . n) is Element of NAT & (F . (n + 1)) is Element of NAT by A24;

            hence (F . n) < (F . (n + 1)) by A20;

          end;

          then

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

          

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

          

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

          proof

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

            assume ex n st P3[n];

            then

             A27: ex n be Nat st P3[n];

            consider M1 be Nat such that

             A28: P3[M1] & for n be Nat st P3[n] holds M1 <= n from NAT_1:sch 5( A27);

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

            

             A29: ex n be Nat st P4[n]

            proof

              take M;

              M <= M1 & M <> M1 by A14, A20, A28;

              hence M < M1 by XXREAL_0: 1;

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

              take 0 ;

              thus thesis by A20;

            end;

            

             A30: for n be Nat st P4[n] holds n <= M1;

            consider MX be Nat such that

             A31: P4[MX] & for n be Nat st P4[n] holds n <= MX from NAT_1:sch 6( A30, A29);

            

             A32: for k st MX < k & k < M1 holds (s2 . k) = x0

            proof

              given k such that

               A33: MX < k and

               A34: k < M1 & (s2 . k) <> x0;

              now

                per cases ;

                  suppose ex m st (F . m) = k;

                  hence contradiction by A31, A33, A34;

                end;

                  suppose for m holds (F . m) <> k;

                  hence contradiction by A28, A34;

                end;

              end;

              hence contradiction;

            end;

            consider m such that

             A35: (F . m) = MX by A31;

            

             A36: MX < (F . (m + 1)) & (s2 . (F . (m + 1))) <> x0 by A20, A35;

            M1 in NAT by ORDINAL1:def 12;

            then

             A37: (F . (m + 1)) <= M1 by A20, A28, A31, A35;

            now

              assume (F . (m + 1)) <> M1;

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

              hence contradiction by A32, A36;

            end;

            hence contradiction by A28;

          end;

          

           A38: for n be Nat holds ((s2 * F) . n) <> x0

          proof

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

            

             A39: for k be Nat st P4[k] holds P4[(k + 1)]

            proof

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

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

               P[k, (F . k), (F . (k + 1))] by A20;

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

              hence thesis by FUNCT_2: 15;

            end;

            

             A40: P4[ 0 ] by A14, A20, FUNCT_2: 15;

            thus for n be Nat holds P4[n] from NAT_1:sch 2( A40, A39);

          end;

          

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

          then ( rng (s2 * F)) c= ( dom f) by A2;

          then

           A42: (f /* (s2 * F)) is convergent & (f . x0) = ( lim (f /* (s2 * F))) by A1, A38, A25;

           A43:

          now

            let p be Real;

            assume

             A44: 0 < p;

            then

            consider n be Nat such that

             A45: for m be Nat st n <= m holds |.(((f /* (s2 * F)) . m) - (f . x0)).| < p by A42, SEQ_2:def 7;

            reconsider k = (F . n) as Nat;

            take k;

            let m be Nat such that

             A46: k <= m;

            

             A47: m in NAT by ORDINAL1:def 12;

            now

              per cases ;

                suppose (s2 . m) = x0;

                

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

                .= 0 by ABSVALUE: 2;

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

              end;

                suppose (s2 . m) <> x0;

                then

                consider l be Element of NAT such that

                 A48: m = (F . l) by A26, A47;

                n <= l by A46, A48, SEQM_3: 1;

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

                then |.((f . ((s2 * F) . l)) - (f . x0)).| < p by A2, A41, FUNCT_2: 108, XBOOLE_1: 1;

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

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

              end;

            end;

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

          end;

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

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

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_1:3

    

     Th3: f is_continuous_in x0 iff 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 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;

        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[ Element of NAT , Real] means $2 in ( dom f) & |.($2 - x0).| < (1 / ($1 + 1)) & not |.((f . $2) - (f . x0)).| < r;

        

         A4: for n holds ex p be Element of REAL st P[n, p]

        proof

          let n;

           0 < ((n + 1) " );

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

          then

          consider p 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 such that

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

        

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

        proof

          let x be object;

          assume x in ( rng s1);

          then ex n st x = (s1 . n) by FUNCT_2: 113;

          hence thesis by A6;

        end;

         A8:

        now

          let n be Nat;

          

           A9: n in NAT by ORDINAL1:def 12;

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

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

        end;

         A10:

        now

          let s be Real;

          assume

           A11: 0 < s;

          consider n be Nat such that

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

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

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

          then

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

          take k = n;

          let m be Nat;

          

           A14: 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 A13, XXREAL_0: 2;

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

        end;

        then

         A15: s1 is convergent by SEQ_2:def 6;

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

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

        then

        consider n be Nat such that

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

        hence contradiction by A8;

      end;

      assume

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

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

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

         A20:

        now

          let p be Real;

          assume 0 < p;

          then

          consider s such that

           A21: 0 < s and

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

          consider n be Nat such that

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

          take k = n;

          let m be Nat;

          

           A24: m in NAT by ORDINAL1:def 12;

          assume k <= m;

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

          then |.((f . (s1 . m)) - (f . x0)).| < p by A18, A22;

          hence |.(((f /* s1) . m) - (f . x0)).| < p by A18, FUNCT_2: 108, A24;

        end;

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

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

      end;

      hence thesis;

    end;

    theorem :: FCONT_1:4

    

     Th4: for f, x0 holds f is_continuous_in x0 iff 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 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;

        let N1 be Neighbourhood of (f . x0);

        consider r such that

         A2: 0 < r and

         A3: N1 = ].((f . x0) - r), ((f . x0) + r).[ by RCOMP_1:def 6;

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

        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;

        hence thesis by A3, RCOMP_1: 1;

      end;

      assume

       A8: 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 = ].((f . x0) - r), ((f . x0) + r).[ as Neighbourhood of (f . x0) by RCOMP_1:def 6;

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

          hence thesis by RCOMP_1: 1;

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

    end;

    theorem :: FCONT_1:5

    

     Th5: for f, x0 holds f is_continuous_in x0 iff 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 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;

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

        take N;

        now

          let r;

          assume r in (f .: N);

          then ex x be Element of REAL st x in ( dom f) & x in N & r = (f . x) by PARTFUN2: 59;

          hence r in N1 by A2;

        end;

        hence thesis;

      end;

      assume

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

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

        take N;

        let x1;

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

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

        hence (f . x1) in N1 by A4;

      end;

      hence thesis by Th4;

    end;

    theorem :: FCONT_1:6

    (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 RCOMP_1: 16;

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

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

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

      end;

      hence thesis by Th5;

    end;

    theorem :: FCONT_1:7

    

     Th7: 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 & (f1 (#) f2) is_continuous_in x0

    proof

      assume

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

      assume that

       A2: f1 is_continuous_in x0 and

       A3: f2 is_continuous_in x0;

      now

        let s1;

        assume that

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

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

        

         A6: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A4, VALUED_1:def 1;

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

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

        then

         A7: ( rng s1) c= ( dom f2) by A4;

        then

         A8: (f2 /* s1) is convergent by A3, A5;

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

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

        then

         A9: ( rng s1) c= ( dom f1) by A4;

        then

         A10: (f1 /* s1) is convergent by A2, A5;

        then ((f1 /* s1) + (f2 /* s1)) is convergent by A8;

        hence ((f1 + f2) /* s1) is convergent by A6, RFUNCT_2: 8;

        

         A11: (f1 . x0) = ( lim (f1 /* s1)) by A2, A5, A9;

        

         A12: (f2 . x0) = ( lim (f2 /* s1)) by A3, A5, A7;

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

        

        hence ((f1 + f2) . x0) = ((f1 . x0) + (f2 . x0)) by VALUED_1:def 1

        .= ( lim ((f1 /* s1) + (f2 /* s1))) by A10, A11, A8, A12, SEQ_2: 6

        .= ( lim ((f1 + f2) /* s1)) by A6, RFUNCT_2: 8;

      end;

      hence (f1 + f2) is_continuous_in x0;

      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, VALUED_1: 12;

        ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1: 12;

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

        then

         A16: ( rng s1) c= ( dom f2) by A13;

        then

         A17: (f2 /* s1) is convergent by A3, A14;

        ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1: 12;

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

        then

         A18: ( rng s1) c= ( dom f1) by A13;

        then

         A19: (f1 /* s1) is convergent by A2, A14;

        then ((f1 /* s1) - (f2 /* s1)) is convergent by A17;

        hence ((f1 - f2) /* s1) is convergent by A15, RFUNCT_2: 8;

        

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

        

         A21: (f2 . x0) = ( lim (f2 /* s1)) by A3, A14, A16;

        x0 in ( dom (f1 - f2)) by A1, VALUED_1: 12;

        

        hence ((f1 - f2) . x0) = ((f1 . x0) - (f2 . x0)) by VALUED_1: 13

        .= ( lim ((f1 /* s1) - (f2 /* s1))) by A19, A20, A17, A21, SEQ_2: 12

        .= ( lim ((f1 - f2) /* s1)) by A15, RFUNCT_2: 8;

      end;

      hence (f1 - f2) is_continuous_in x0;

      let s1;

      assume that

       A22: ( rng s1) c= ( dom (f1 (#) f2)) and

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

      ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

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

      then

       A24: ( rng s1) c= ( dom f2) by A22;

      then

       A25: (f2 /* s1) is convergent by A3, A23;

      

       A26: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A22, VALUED_1:def 4;

      ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

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

      then

       A27: ( rng s1) c= ( dom f1) by A22;

      then

       A28: (f1 /* s1) is convergent by A2, A23;

      then ((f1 /* s1) (#) (f2 /* s1)) is convergent by A25;

      hence ((f1 (#) f2) /* s1) is convergent by A26, RFUNCT_2: 8;

      

       A29: (f1 . x0) = ( lim (f1 /* s1)) by A2, A23, A27;

      

       A30: (f2 . x0) = ( lim (f2 /* s1)) by A3, A23, A24;

      

      thus ((f1 (#) f2) . x0) = ((f1 . x0) * (f2 . x0)) by VALUED_1: 5

      .= ( lim ((f1 /* s1) (#) (f2 /* s1))) by A28, A29, A25, A30, SEQ_2: 15

      .= ( lim ((f1 (#) f2) /* s1)) by A26, RFUNCT_2: 8;

    end;

    theorem :: FCONT_1:8

    

     Th8: x0 in ( dom f) & f is_continuous_in x0 implies (r (#) f) is_continuous_in x0

    proof

      assume x0 in ( dom f);

      then

       A1: x0 in ( dom (r (#) f)) by VALUED_1:def 5;

      assume

       A2: f is_continuous_in x0;

      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, VALUED_1:def 5;

      then

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

      

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

      then (r (#) (f /* s1)) is convergent;

      hence ((r (#) f) /* s1) is convergent by A5, RFUNCT_2: 9;

      

      thus ((r (#) f) . x0) = (r * (f . x0)) by A1, VALUED_1:def 5

      .= ( lim (r (#) (f /* s1))) by A7, A6, SEQ_2: 8

      .= ( lim ((r (#) f) /* s1)) by A5, RFUNCT_2: 9;

    end;

    theorem :: FCONT_1:9

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

    proof

      assume

       A1: x0 in ( dom f);

      assume

       A2: f is_continuous_in x0;

      now

        let s1;

        assume that

         A3: ( rng s1) c= ( dom ( abs f)) and

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

        

         A5: ( rng s1) c= ( dom f) by A3, VALUED_1:def 11;

        then

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

        

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

        then ( abs (f /* s1)) is convergent by SEQ_4: 13;

        hence (( abs f) /* s1) is convergent by A5, RFUNCT_2: 10;

        

        thus (( abs f) . x0) = |.(f . x0).| by VALUED_1: 18

        .= ( lim ( abs (f /* s1))) by A7, A6, SEQ_4: 14

        .= ( lim (( abs f) /* s1)) by A5, RFUNCT_2: 10;

      end;

      hence ( abs f) is_continuous_in x0;

      thus thesis by A1, A2, Th8;

    end;

    theorem :: FCONT_1:10

    

     Th10: f is_continuous_in x0 & (f . x0) <> 0 implies (f ^ ) is_continuous_in x0

    proof

      assume that

       A1: f is_continuous_in x0 and

       A2: (f . x0) <> 0 ;

       not (f . x0) in { 0 } by A2, TARSKI:def 1;

      then

       A3: not x0 in (f " { 0 }) by FUNCT_1:def 7;

      let s1;

      assume that

       A4: ( rng s1) c= ( dom (f ^ )) and

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

      (( dom f) \ (f " { 0 })) c= ( dom f) & ( rng s1) c= (( dom f) \ (f " { 0 })) by A4, RFUNCT_1:def 2, XBOOLE_1: 36;

      then ( rng s1) c= ( dom f);

      then

       A6: (f /* s1) is convergent & (f . x0) = ( lim (f /* s1)) by A1, A5;

      then ((f /* s1) " ) is convergent by A2, A4, RFUNCT_2: 11, SEQ_2: 21;

      hence ((f ^ ) /* s1) is convergent by A4, RFUNCT_2: 12;

      x0 in ( dom f) by A2, FUNCT_1:def 2;

      then x0 in (( dom f) \ (f " { 0 })) by A3, XBOOLE_0:def 5;

      then x0 in ( dom (f ^ )) by RFUNCT_1:def 2;

      

      hence ((f ^ ) . x0) = ((f . x0) " ) by RFUNCT_1:def 2

      .= ( lim ((f /* s1) " )) by A2, A4, A6, RFUNCT_2: 11, SEQ_2: 22

      .= ( lim ((f ^ ) /* s1)) by A4, RFUNCT_2: 12;

    end;

    theorem :: FCONT_1:11

    x0 in ( dom f2) & f1 is_continuous_in x0 & (f1 . x0) <> 0 & f2 is_continuous_in x0 implies (f2 / f1) is_continuous_in x0

    proof

      assume

       A1: x0 in ( dom f2);

      assume that

       A2: f1 is_continuous_in x0 and

       A3: (f1 . x0) <> 0 and

       A4: f2 is_continuous_in x0;

       not (f1 . x0) in { 0 } by A3, TARSKI:def 1;

      then

       A5: not x0 in (f1 " { 0 }) by FUNCT_1:def 7;

      x0 in ( dom f1) by A3, FUNCT_1:def 2;

      then x0 in (( dom f1) \ (f1 " { 0 })) by A5, XBOOLE_0:def 5;

      then x0 in ( dom (f1 ^ )) by RFUNCT_1:def 2;

      then

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

      (f1 ^ ) is_continuous_in x0 by A2, A3, Th10;

      then (f2 (#) (f1 ^ )) is_continuous_in x0 by A4, A6, Th7;

      hence thesis by RFUNCT_1: 31;

    end;

    theorem :: FCONT_1:12

    

     Th12: x0 in ( dom (f2 * f1)) & f1 is_continuous_in x0 & f2 is_continuous_in (f1 . x0) implies (f2 * f1) is_continuous_in x0

    proof

      assume

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

      assume that

       A2: f1 is_continuous_in x0 and

       A3: f2 is_continuous_in (f1 . x0);

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

      now

        let n;

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

        then

         A9: (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 A9, 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

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

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

      then

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

      then (f2 . (f1 . x0)) = ( lim (f2 /* (f1 /* s1))) by A3, A8;

      hence thesis by A1, A3, A11, A8, A10, FUNCT_1: 12;

    end;

    definition

      let f;

      :: FCONT_1:def2

      attr f is continuous means

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

    end

    theorem :: FCONT_1:13

    

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

        now

          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;

            

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

            

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

            .= (f . (s1 . n)) by A3, A6, A8, FUNCT_1: 47

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

          end;

          then

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

          (f . ( lim s1)) = ((f | X) . ( lim s1)) by A5, A6, FUNCT_1: 47

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

        hence thesis;

      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;

            

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

            

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

            .= (f . (s1 . n)) by A13, A16, FUNCT_1: 47

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

          end;

          then

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

          ((f | X) . ( lim s1)) = (f . ( lim s1)) by A12, A15, FUNCT_1: 47

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

      end;

      hence thesis;

    end;

    theorem :: FCONT_1:14

    

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

    proof

      assume

       A1: X c= ( dom f);

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

      proof

        assume

         A2: (f | X) is continuous;

        let x0, r;

        assume that

         A3: x0 in X and

         A4: 0 < r;

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

        then (f | X) is_continuous_in x0 by A2;

        then

        consider s such that

         A5: 0 < s and

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

        take s;

        thus 0 < s by A5;

        let x1;

        assume that

         A7: x1 in X and

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

        

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

        .= X by A1, XBOOLE_1: 28;

        

        then |.((f . x1) - (f . x0)).| = |.(((f | X) . x1) - (f . x0)).| by A7, FUNCT_1: 47

        .= |.(((f | X) . x1) - ((f | X) . x0)).| by A3, A9, FUNCT_1: 47;

        hence thesis by A6, A9, A7, A8;

      end;

      assume

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

      now

        let x0 such that

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

        

         A12: x0 in X by A11;

        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

           A13: 0 < s and

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

          take s;

          thus 0 < s by A13;

          let x1 such that

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

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

           |.(((f | X) . x1) - ((f | X) . x0)).| = |.(((f | X) . x1) - (f . x0)).| by A11, FUNCT_1: 47

          .= |.((f . x1) - (f . x0)).| by A15, FUNCT_1: 47;

          hence thesis by A14, A15, A16;

        end;

        hence (f | X) is_continuous_in x0 by Th3;

      end;

      hence thesis;

    end;

    registration

      cluster constant -> continuous for PartFunc of REAL , REAL ;

      coherence

      proof

        let f be PartFunc of REAL , REAL ;

        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 . x0) by A1, A2, A4;

          hence |.((f . x1) - (f . x0)).| < r by A3, ABSVALUE: 2;

        end;

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

        hence thesis;

      end;

    end

    registration

      cluster continuous for PartFunc of REAL , REAL ;

      existence

      proof

        set f = the constant PartFunc of REAL , REAL ;

        take f;

        thus thesis;

      end;

    end

    registration

      let f be continuous PartFunc of REAL , REAL , X be set;

      cluster (f | X) -> continuous;

      coherence

      proof

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

        proof

          let x0;

          assume

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

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

          then

           A2: f is_continuous_in x0 by Def2;

          x0 in X by A1;

          hence thesis by A2, Th1;

        end;

        hence thesis;

      end;

    end

    theorem :: FCONT_1:15

    (f | X) is continuous iff ((f | X) | X) is continuous;

    theorem :: FCONT_1:16

    

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

      cluster empty -> continuous for PartFunc of REAL , REAL ;

      coherence ;

    end

    registration

      let f;

      let X be trivial set;

      cluster (f | X) -> continuous;

      coherence

      proof

        per cases ;

          suppose (f | X) is empty;

          hence thesis;

        end;

          suppose not (f | X) is empty;

          then

          consider x0 such that

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

          x0 in X by A1, RELAT_1: 57;

          then

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

          now

            let p;

            assume p in ( dom (f | X));

            then

             A3: p in {x0} by A2;

            thus (f | X) is_continuous_in p

            proof

              let s1;

              assume that

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

              

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

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

              then

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

               A7:

              now

                let n;

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

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

              end;

              

               A8: p = x0 by A3, 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 A2, A8, A4, FUNCT_2: 108, A11

                .= |.(((f | {x0}) . x0) - ((f | {x0}) . x0)).| by A7, A11

                .= 0 by ABSVALUE: 2;

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

              end;

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

              hence thesis by A2, A9, SEQ_2:def 7;

            end;

          end;

          hence thesis;

        end;

      end;

    end

    theorem :: FCONT_1:17

    (f | {x0}) is continuous;

    registration

      let f1,f2 be continuous PartFunc of REAL , REAL ;

      cluster (f1 + f2) -> continuous;

      coherence

      proof

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

        X c= (( dom f1) /\ ( dom f2)) by VALUED_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, Th13;

          then

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

          

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

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

          

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

          .= ( lim ((f1 /* s1) + (f2 /* s1))) by A6, SEQ_2: 6

          .= ( lim ((f1 + f2) /* s1)) by A8, RFUNCT_2: 8;

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

        end;

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

        hence thesis;

      end;

      cluster (f1 - f2) -> continuous;

      coherence

      proof

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

        X c= (( dom f1) /\ ( dom f2)) by VALUED_1: 12;

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

          then

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

          

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

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

          

          then ((f1 - f2) . ( lim s1)) = (( lim (f1 /* s1)) - ( lim (f2 /* s1))) by A13, VALUED_1: 13

          .= ( lim ((f1 /* s1) - (f2 /* s1))) by A14, SEQ_2: 12

          .= ( lim ((f1 - f2) /* s1)) by A16, RFUNCT_2: 8;

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

        end;

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

        hence thesis;

      end;

      cluster (f1 (#) f2) -> continuous;

      coherence

      proof

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

        X c= (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

        then

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

        

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

        now

          let s1;

          assume that

           A19: ( rng s1) c= X and

           A20: s1 is convergent and

           A21: ( lim s1) in X;

          

           A22: (f1 /* s1) is convergent & (f2 /* s1) is convergent by A17, A18, A19, A20, A21, Th13;

          then

           A23: ((f1 /* s1) (#) (f2 /* s1)) is convergent;

          

           A24: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A19, VALUED_1:def 4;

          (f1 . ( lim s1)) = ( lim (f1 /* s1)) & (f2 . ( lim s1)) = ( lim (f2 /* s1)) by A17, A18, A19, A20, A21, Th13;

          

          then ((f1 (#) f2) . ( lim s1)) = (( lim (f1 /* s1)) * ( lim (f2 /* s1))) by A21, VALUED_1:def 4

          .= ( lim ((f1 /* s1) (#) (f2 /* s1))) by A22, SEQ_2: 15

          .= ( lim ((f1 (#) f2) /* s1)) by A24, RFUNCT_2: 8;

          hence ((f1 (#) f2) /* s1) is convergent & ((f1 (#) f2) . ( lim s1)) = ( lim ((f1 (#) f2) /* s1)) by A24, A23, RFUNCT_2: 8;

        end;

        then ((f1 (#) f2) | X) is continuous by Th13;

        hence thesis;

      end;

    end

    theorem :: FCONT_1:18

    

     Th18: 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 & ((f1 (#) f2) | X) is continuous

    proof

      let X, f1, f2 such that

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

      assume

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

      

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

       A4:

      now

        let s1;

        assume that

         A5: ( rng s1) c= X and

         A6: s1 is convergent & ( lim s1) in X;

        

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

        

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

        then

         A9: ((f1 /* s1) (#) (f2 /* s1)) is convergent;

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

        

        then ((f1 (#) f2) . ( lim s1)) = (( lim (f1 /* s1)) * ( lim (f2 /* s1))) by VALUED_1: 5

        .= ( lim ((f1 /* s1) (#) (f2 /* s1))) by A8, SEQ_2: 15

        .= ( lim ((f1 (#) f2) /* s1)) by A7, RFUNCT_2: 8;

        hence ((f1 (#) f2) /* s1) is convergent & ((f1 (#) f2) . ( lim s1)) = ( lim ((f1 (#) f2) /* s1)) by A7, A9, RFUNCT_2: 8;

      end;

      

       A10: X c= ( dom (f1 + f2)) by A1, VALUED_1:def 1;

      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 A3, A2, A11, A12, A13, Th13;

        then

         A15: ((f1 /* s1) + (f2 /* s1)) is convergent;

        

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

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

        

        then ((f1 + f2) . ( lim s1)) = (( lim (f1 /* s1)) + ( lim (f2 /* s1))) by A10, A13, VALUED_1:def 1

        .= ( lim ((f1 /* s1) + (f2 /* s1))) by A14, SEQ_2: 6

        .= ( lim ((f1 + f2) /* s1)) by A16, RFUNCT_2: 8;

        hence ((f1 + f2) /* s1) is convergent & ((f1 + f2) . ( lim s1)) = ( lim ((f1 + f2) /* s1)) by A16, A15, RFUNCT_2: 8;

      end;

      hence ((f1 + f2) | X) is continuous by A10, Th13;

      

       A17: X c= ( dom (f1 - f2)) by A1, VALUED_1: 12;

      now

        let s1;

        assume that

         A18: ( rng s1) c= X and

         A19: s1 is convergent and

         A20: ( lim s1) in X;

        

         A21: (f1 /* s1) is convergent & (f2 /* s1) is convergent by A3, A2, A18, A19, A20, Th13;

        then

         A22: ((f1 /* s1) - (f2 /* s1)) is convergent;

        

         A23: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A1, A18;

        (f1 . ( lim s1)) = ( lim (f1 /* s1)) & (f2 . ( lim s1)) = ( lim (f2 /* s1)) by A3, A2, A18, A19, A20, Th13;

        

        then ((f1 - f2) . ( lim s1)) = (( lim (f1 /* s1)) - ( lim (f2 /* s1))) by A17, A20, VALUED_1: 13

        .= ( lim ((f1 /* s1) - (f2 /* s1))) by A21, SEQ_2: 12

        .= ( lim ((f1 - f2) /* s1)) by A23, RFUNCT_2: 8;

        hence ((f1 - f2) /* s1) is convergent & ((f1 - f2) . ( lim s1)) = ( lim ((f1 - f2) /* s1)) by A23, A22, RFUNCT_2: 8;

      end;

      hence ((f1 - f2) | X) is continuous by A17, Th13;

      X c= ( dom (f1 (#) f2)) by A1, VALUED_1:def 4;

      hence thesis by A4, Th13;

    end;

    theorem :: FCONT_1:19

    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 & ((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 Th16, XBOOLE_1: 17;

      hence thesis by A1, Th18;

    end;

    registration

      let f be continuous PartFunc of REAL , REAL ;

      let r;

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

      coherence

      proof

        set X = ( dom f);

        

         A1: X c= ( dom (r (#) f)) by VALUED_1:def 5;

        

         A2: (f | X) is continuous;

         A3:

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

          then

           A8: (r (#) (f /* s1)) is convergent;

          (f . ( lim s1)) = ( lim (f /* s1)) by A2, A4, A5, A6, Th13;

          

          then ((r (#) f) . ( lim s1)) = (r * ( lim (f /* s1))) by A1, A6, VALUED_1:def 5

          .= ( lim (r (#) (f /* s1))) by A7, SEQ_2: 8

          .= ( lim ((r (#) f) /* s1)) by A4, RFUNCT_2: 9;

          hence ((r (#) f) /* s1) is convergent & ((r (#) f) . ( lim s1)) = ( lim ((r (#) f) /* s1)) by A4, A8, RFUNCT_2: 9;

        end;

        ( dom (r (#) f)) = X by VALUED_1:def 5;

        then ((r (#) f) | X) = (r (#) f);

        hence thesis by A1, A3, Th13;

      end;

    end

    theorem :: FCONT_1:20

    

     Th20: for r, X, f st X c= ( dom f) & (f | X) is continuous holds ((r (#) f) | X) is continuous

    proof

      let r, X, f such that

       A1: X c= ( dom f);

      assume

       A2: (f | X) is continuous;

      

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

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

        then

         A8: (r (#) (f /* s1)) is convergent;

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

        

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

        .= ( lim (r (#) (f /* s1))) by A7, SEQ_2: 8

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

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

      end;

      hence thesis by A3, Th13;

    end;

    theorem :: FCONT_1:21

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

    proof

      assume

       A1: X c= ( dom f);

      assume

       A2: (f | X) is continuous;

      thus (( abs f) | X) is continuous

      proof

        let r;

        assume

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

        then r in ( dom ( abs f)) by RELAT_1: 57;

        then

         A4: r in ( dom f) by VALUED_1:def 11;

        r in X by A3;

        then

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

        then

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

        thus (( abs f) | X) is_continuous_in r

        proof

          let s1;

          assume that

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

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

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

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

          then

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

          now

            let n;

            

             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 by XBOOLE_0:def 4;

            

            thus (( abs ((f | X) /* s1)) . n) = |.(((f | X) /* s1) . n).| by SEQ_1: 12

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

            .= |.(f . (s1 . n)).| by A9, A10, FUNCT_1: 47

            .= (( abs f) . (s1 . n)) by VALUED_1: 18

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

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

          end;

          then

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

          

           A13: |.((f | X) . r).| = |.(f . r).| by A5, FUNCT_1: 47

          .= (( abs f) . r) by VALUED_1: 18

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

          

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

          hence ((( abs f) | X) /* s1) is convergent by A12, SEQ_4: 13;

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

          hence thesis by A14, A12, A13, SEQ_4: 14;

        end;

      end;

      thus thesis by A1, A2, Th20;

    end;

    theorem :: FCONT_1:22

    

     Th22: (f | X) is continuous & (f " { 0 }) = {} implies ((f ^ ) | X) is continuous

    proof

      assume that

       A1: (f | X) is continuous and

       A2: (f " { 0 }) = {} ;

      

       A3: ( dom (f ^ )) = (( dom f) \ {} ) by A2, RFUNCT_1:def 2

      .= ( dom f);

      let r;

      assume

       A4: r in ( dom ((f ^ ) | X));

      then

       A5: r in ( dom (f ^ )) by RELAT_1: 57;

      r in X by A4;

      then

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

      then

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

      now

         A8:

        now

          assume (f . r) = 0 ;

          then (f . r) in { 0 } by TARSKI:def 1;

          hence contradiction by A2, A3, A5, FUNCT_1:def 7;

        end;

        let s1;

        assume that

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

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

        ( rng s1) c= (( dom (f ^ )) /\ X) by A9, RELAT_1: 61;

        then

         A11: ( rng s1) c= ( dom (f | X)) by A3, RELAT_1: 61;

        then

         A12: ((f | X) /* s1) is convergent by A7, A10;

        now

          let n be Nat;

          

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

          ( rng s1) c= (( dom f) /\ X) & (( dom f) /\ X) c= ( dom f) by A3, A9, RELAT_1: 61, XBOOLE_1: 17;

          then

           A14: ( rng s1) c= ( dom f);

           A15:

          now

            assume (f . (s1 . n)) = 0 ;

            then (f . (s1 . n)) in { 0 } by TARSKI:def 1;

            hence contradiction by A2, A14, A13, FUNCT_1:def 7;

          end;

          n in NAT by ORDINAL1:def 12;

          

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

          .= (f . (s1 . n)) by A11, A13, FUNCT_1: 47;

          hence (((f | X) /* s1) . n) <> 0 by A15;

        end;

        then

         A16: ((f | X) /* s1) is non-zero by SEQ_1: 5;

        now

          let n;

          

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

           A18: (s1 . n) in ( dom (f ^ )) by XBOOLE_0:def 4;

          

          thus ((((f ^ ) | X) /* s1) . n) = (((f ^ ) | X) . (s1 . n)) by A9, FUNCT_2: 108

          .= ((f ^ ) . (s1 . n)) by A9, A17, FUNCT_1: 47

          .= ((f . (s1 . n)) " ) by A18, RFUNCT_1:def 2

          .= (((f | X) . (s1 . n)) " ) by A11, A17, FUNCT_1: 47

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

          .= ((((f | X) /* s1) " ) . n) by VALUED_1: 10;

        end;

        then

         A19: (((f ^ ) | X) /* s1) = (((f | X) /* s1) " ) by FUNCT_2: 63;

        

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

        then ( lim ((f | X) /* s1)) <> 0 by A7, A10, A11, A8;

        hence (((f ^ ) | X) /* s1) is convergent by A12, A16, A19, SEQ_2: 21;

        ((f | X) . r) = ( lim ((f | X) /* s1)) by A7, A10, A11;

        

        hence ( lim (((f ^ ) | X) /* s1)) = (((f | X) . r) " ) by A12, A20, A8, A16, A19, SEQ_2: 22

        .= ((f . r) " ) by A6, FUNCT_1: 47

        .= ((f ^ ) . r) by A5, RFUNCT_1:def 2

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

      end;

      hence thesis;

    end;

    theorem :: FCONT_1:23

    (f | X) is continuous & ((f | X) " { 0 }) = {} implies ((f ^ ) | X) is continuous

    proof

      assume that

       A1: (f | X) is continuous and

       A2: ((f | X) " { 0 }) = {} ;

      ((f | X) | X) is continuous by A1;

      then (((f | X) ^ ) | X) is continuous by A2, Th22;

      then (((f ^ ) | X) | X) is continuous by RFUNCT_1: 46;

      hence thesis;

    end;

    theorem :: FCONT_1:24

    X c= (( dom f1) /\ ( dom f2)) & (f1 | X) is continuous & (f1 " { 0 }) = {} & (f2 | X) is continuous implies ((f2 / f1) | X) is continuous

    proof

      assume

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

      assume that

       A2: (f1 | X) is continuous and

       A3: (f1 " { 0 }) = {} and

       A4: (f2 | X) is continuous;

      

       A5: ( dom (f1 ^ )) = (( dom f1) \ {} ) by A3, RFUNCT_1:def 2

      .= ( dom f1);

      ((f1 ^ ) | X) is continuous by A2, A3, Th22;

      then ((f2 (#) (f1 ^ )) | X) is continuous by A1, A4, A5, Th18;

      hence thesis by RFUNCT_1: 31;

    end;

    registration

      let f1,f2 be continuous PartFunc of REAL , REAL ;

      cluster (f2 * f1) -> continuous;

      coherence

      proof

        now

          let x0;

          assume

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

          then (f1 . x0) in ( dom f2) by FUNCT_1: 11;

          then

           A2: f2 is_continuous_in (f1 . x0) by Def2;

          x0 in ( dom f1) by A1, FUNCT_1: 11;

          then f1 is_continuous_in x0 by Def2;

          hence (f2 * f1) is_continuous_in x0 by A1, A2, Th12;

        end;

        hence thesis;

      end;

    end

    theorem :: FCONT_1:25

    (f1 | X) is continuous & (f2 | (f1 .: X)) is continuous implies ((f2 * f1) | X) is continuous

    proof

      ((f2 * f1) | X) = ((f2 | (f1 .: X)) * (f1 | X)) by FUNCT_1: 99;

      hence thesis;

    end;

    theorem :: FCONT_1:26

    (f1 | X) is continuous & (f2 | X1) is continuous implies ((f2 * f1) | (X /\ (f1 " X1))) is continuous

    proof

      ((f2 | X1) * (f1 | X)) = ((f2 * f1) | (X /\ (f1 " X1))) by FUNCT_1: 100;

      hence thesis;

    end;

    theorem :: FCONT_1:27

    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;

      

       A5: ((f . x0) + 0 qua Nat) = (f . (x0 + 0 qua Nat))

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

       A6:

      now

        let x1;

         0 = (f . (x1 + ( - x1))) by A5

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

        hence ( - (f . x1)) = (f . ( - x1));

      end;

       A7:

      now

        let x1, x2;

        

        thus (f . (x1 - x2)) = (f . (x1 + ( - x2)))

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

        .= ((f . x1) + ( - (f . x2))) by A6

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

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

        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)).|

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

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

      end;

      hence thesis by A3, Th14;

    end;

    theorem :: FCONT_1:28

    

     Th28: for f st ( dom f) is compact & (f | ( dom f)) is continuous holds ( rng f) is compact

    proof

      let f;

      assume that

       A1: ( dom f) is compact and

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

      now

        let s1 such that

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

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

        

         A4: for n holds ex p be Element of REAL st P[n, p]

        proof

          let n;

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

          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;

        end;

        consider q1 such that

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

        now

          let x be object;

          assume x in ( rng q1);

          then ex n st x = (q1 . n) by FUNCT_2: 113;

          hence x in ( dom f) by A6;

        end;

        then

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

        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;

        now

          let n;

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

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

        end;

        then

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

        take q2 = (f /* s2);

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

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

        then

         A12: f is_continuous_in ( lim s2);

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

        then

         A13: ( rng s2) c= ( dom f) by A7;

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

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

      end;

      hence thesis by RCOMP_1:def 3;

    end;

    theorem :: FCONT_1:29

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

      hence thesis by RELAT_1: 115;

    end;

    theorem :: FCONT_1:30

    

     Th30: for f st ( dom f) <> {} & ( dom f) is compact & (f | ( dom f)) is continuous 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;

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

      then

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

      then

      consider x be Element of REAL 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 REAL 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;

    end;

    ::$Notion-Name

    theorem :: FCONT_1:31

    for f, Y st Y <> {} & Y c= ( dom f) & Y is compact & (f | Y) is continuous 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 | Y) is continuous;

      

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

      .= Y by A2, XBOOLE_1: 28;

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

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

      take x1, x2;

      thus x1 in Y & x2 in Y by A6;

      (f . x1) = ( upper_bound ( rng (f | Y))) & (f . x2) = ( lower_bound ( rng (f | Y))) by A6, A7, FUNCT_1: 47;

      hence thesis by RELAT_1: 115;

    end;

    definition

      let f;

      :: FCONT_1:def3

      attr f is Lipschitzian means

      : Def3: ex r 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 :: FCONT_1:32

    

     Th32: (f | X) is Lipschitzian iff ex r 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 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 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;

        assume

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

        then ((f | X) . x1) = (f . x1) & ((f | X) . x2) = (f . x2) by FUNCT_1: 47;

        hence thesis by A2, A3;

      end;

      given r such that

       A4: 0 < r and

       A5: 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 A4;

      let x1, x2;

      assume

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

      then ((f | X) . x1) = (f . x1) & ((f | X) . x2) = (f . x2) by FUNCT_1: 47;

      hence thesis by A5, A6;

    end;

    registration

      cluster empty -> Lipschitzian for PartFunc of REAL , REAL ;

      coherence

      proof

        let f be PartFunc of REAL , REAL ;

        assume

         A1: f is empty;

        take 1;

        thus thesis by A1;

      end;

    end

    registration

      cluster empty for PartFunc of REAL , REAL ;

      existence

      proof

        take the empty PartFunc of REAL , REAL ;

        thus thesis;

      end;

    end

    registration

      let f be Lipschitzian PartFunc of REAL , REAL , X be set;

      cluster (f | X) -> Lipschitzian;

      coherence

      proof

        consider r 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, Th32;

      end;

    end

    theorem :: FCONT_1:33

    (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 f1,f2 be Lipschitzian PartFunc of REAL , REAL ;

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

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

        now

          take p = (s + g);

          thus 0 < p by A1, A3;

          let x1, x2;

          assume that

           A5: x1 in ( dom (f1 + f2)) and

           A6: x2 in ( dom (f1 + f2));

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

          .= |.(((f1 . x1) + (f2 . x1)) - ((f1 . x2) + (f2 . x2))).| by A6, VALUED_1:def 1

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

          then

           A7: |.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| <= ( |.((f1 . x1) - (f1 . x2)).| + |.((f2 . x1) - (f2 . x2)).|) by COMPLEX1: 56;

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

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

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

          then

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

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

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

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

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

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

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

        end;

        hence thesis;

      end;

      cluster (f1 - f2) -> Lipschitzian;

      coherence

      proof

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

        consider s such that

         A9: 0 < s and

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

        consider g such that

         A11: 0 < g and

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

        now

          take p = (s + g);

          thus 0 < p by A9, A11;

          let x1, x2;

          assume that

           A13: x1 in ( dom (f1 - f2)) and

           A14: x2 in ( dom (f1 - f2));

           |.(((f1 - f2) . x1) - ((f1 - f2) . x2)).| = |.(((f1 . x1) - (f2 . x1)) - ((f1 - f2) . x2)).| by A13, VALUED_1: 13

          .= |.(((f1 . x1) - (f2 . x1)) - ((f1 . x2) - (f2 . x2))).| by A14, VALUED_1: 13

          .= |.(((f1 . x1) - (f1 . x2)) - ((f2 . x1) - (f2 . x2))).|;

          then

           A15: |.(((f1 - f2) . x1) - ((f1 - f2) . x2)).| <= ( |.((f1 . x1) - (f1 . x2)).| + |.((f2 . x1) - (f2 . x2)).|) by COMPLEX1: 57;

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

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

          .= ( dom (f1 - f2)) by VALUED_1: 12;

          then

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

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

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

          .= ( dom (f1 - f2)) by VALUED_1: 12;

          then |.((f1 . x1) - (f1 . x2)).| <= (s * |.(x1 - x2).|) by A10, A13, A14;

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

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

        end;

        hence thesis;

      end;

    end

    theorem :: FCONT_1:34

    (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 RFUNCT_1: 44;

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

      hence thesis by A1, A2;

    end;

    theorem :: FCONT_1:35

    (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 RFUNCT_1: 47;

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

      hence thesis by A1, A2;

    end;

    registration

      let f1,f2 be bounded Lipschitzian PartFunc of REAL , REAL ;

      cluster (f1 (#) f2) -> Lipschitzian;

      coherence

      proof

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

        consider x1 such that

         A1: for r be object st r in ( dom f1) holds |.(f1 . r).| <= x1 by RFUNCT_1: 72;

        consider x2 such that

         A2: for r be object st r in ( dom f2) holds |.(f2 . r).| <= x2 by RFUNCT_1: 72;

        consider g such that

         A3: 0 < g and

         A4: for x1, x2 st x1 in ( dom f2) & x2 in ( dom f2) holds |.((f2 . x1) - (f2 . x2)).| <= (g * |.(x1 - x2).|) by Def3;

        consider s such that

         A5: 0 < s and

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

         A7:

        now

          let r;

          assume r in ( dom (f1 (#) f2));

          then

           A8: r in (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

          then r in ( dom f1) by XBOOLE_0:def 4;

          then

           A9: |.(f1 . r).| <= x1 by A1;

          r in ( dom f2) by A8, XBOOLE_0:def 4;

          then

           A10: |.(f2 . r).| <= x2 by A2;

          x1 <= |.x1.| by ABSVALUE: 4;

          hence |.(f1 . r).| <= |.x1.| by A9, XXREAL_0: 2;

          x2 <= |.x2.| by ABSVALUE: 4;

          hence |.(f2 . r).| <= |.x2.| by A10, XXREAL_0: 2;

        end;

        now

          take p = ((( |.x1.| * g) + ( |.x2.| * s)) + 1);

          

           A11: 0 <= |.x1.| by COMPLEX1: 46;

           0 <= |.x1.| & 0 <= |.x2.| by COMPLEX1: 46;

          hence 0 < p by A5, A3;

          let y1,y2 be Real;

          assume that

           A12: y1 in ( dom (f1 (#) f2)) and

           A13: y2 in ( dom (f1 (#) f2));

          

           A14: y2 in (X /\ X1) by A13, VALUED_1:def 4;

          then

           A15: y2 in X by XBOOLE_0:def 4;

           |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| = ( |.(f1 . y1).| * |.((f2 . y1) - (f2 . y2)).|) & 0 <= |.((f2 . y1) - (f2 . y2)).| by COMPLEX1: 46, COMPLEX1: 65;

          then

           A16: |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| <= ( |.x1.| * |.((f2 . y1) - (f2 . y2)).|) by A7, A12, XREAL_1: 64;

          

           A17: y2 in X1 by A14, XBOOLE_0:def 4;

          

           A18: y1 in (X /\ X1) by A12, VALUED_1:def 4;

          then y1 in X1 by XBOOLE_0:def 4;

          then ( |.x1.| * |.((f2 . y1) - (f2 . y2)).|) <= ( |.x1.| * (g * |.(y1 - y2).|)) by A4, A17, A11, XREAL_1: 64;

          then

           A19: |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| <= (( |.x1.| * g) * |.(y1 - y2).|) by A16, XXREAL_0: 2;

           0 <= |.(y1 - y2).| by COMPLEX1: 46;

          then

           A20: (((( |.x1.| * g) + ( |.x2.| * s)) * |.(y1 - y2).|) + 0 qua Nat) <= (((( |.x1.| * g) + ( |.x2.| * s)) * |.(y1 - y2).|) + (1 * |.(y1 - y2).|)) by XREAL_1: 7;

           |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| = |.(((f1 . y1) * (f2 . y1)) - ((f1 (#) f2) . y2)).| by VALUED_1: 5

          .= |.((((f1 . y1) * (f2 . y1)) + (((f1 . y1) * (f2 . y2)) - ((f1 . y1) * (f2 . y2)))) - ((f1 . y2) * (f2 . y2))).| by VALUED_1: 5

          .= |.(((f1 . y1) * ((f2 . y1) - (f2 . y2))) + (((f1 . y1) - (f1 . y2)) * (f2 . y2))).|;

          then

           A21: |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= ( |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| + |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).|) by COMPLEX1: 56;

           |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| = ( |.(f2 . y2).| * |.((f1 . y1) - (f1 . y2)).|) & 0 <= |.((f1 . y1) - (f1 . y2)).| by COMPLEX1: 46, COMPLEX1: 65;

          then

           A22: |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| <= ( |.x2.| * |.((f1 . y1) - (f1 . y2)).|) by A7, A13, XREAL_1: 64;

          

           A23: 0 <= |.x2.| by COMPLEX1: 46;

          y1 in X by A18, XBOOLE_0:def 4;

          then ( |.x2.| * |.((f1 . y1) - (f1 . y2)).|) <= ( |.x2.| * (s * |.(y1 - y2).|)) by A6, A15, A23, XREAL_1: 64;

          then |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| <= ( |.x2.| * (s * |.(y1 - y2).|)) by A22, XXREAL_0: 2;

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

          then |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= ((( |.x1.| * g) + ( |.x2.| * s)) * |.(y1 - y2).|) by A21, XXREAL_0: 2;

          hence |.(((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)).| <= (p * |.(y1 - y2).|) by A20, XXREAL_0: 2;

        end;

        hence thesis;

      end;

    end

    theorem :: FCONT_1:36

    (f1 | X) is Lipschitzian & (f2 | X1) is Lipschitzian & (f1 | Z) is bounded & (f2 | Z1) is bounded implies ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) is Lipschitzian

    proof

      

       A1: (f1 | (((X /\ Z) /\ X1) /\ Z1)) = (f1 | ((X1 /\ Z1) /\ (X /\ Z))) by XBOOLE_1: 16

      .= (f1 | (((X1 /\ Z1) /\ X) /\ Z)) by XBOOLE_1: 16

      .= ((f1 | Z) | ((X1 /\ Z1) /\ X)) by RELAT_1: 71;

      

       A2: (f1 | (((X /\ Z) /\ X1) /\ Z1)) = (f1 | ((X1 /\ Z1) /\ (X /\ Z))) by XBOOLE_1: 16

      .= (f1 | (((X1 /\ Z1) /\ Z) /\ X)) by XBOOLE_1: 16

      .= ((f1 | X) | ((X1 /\ Z1) /\ Z)) by RELAT_1: 71;

      

       A3: (f2 | (((X /\ Z) /\ X1) /\ Z1)) = (f2 | (((X /\ Z) /\ Z1) /\ X1)) by XBOOLE_1: 16

      .= ((f2 | X1) | ((Z /\ X) /\ Z1)) by RELAT_1: 71;

      

       A4: ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) = ((f1 | (((X /\ Z) /\ X1) /\ Z1)) (#) (f2 | (((X /\ Z) /\ X1) /\ Z1))) & (f2 | (((X /\ Z) /\ X1) /\ Z1)) = ((f2 | Z1) | ((X /\ Z) /\ X1)) by RELAT_1: 71, RFUNCT_1: 45;

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

      hence thesis by A1, A2, A4, A3;

    end;

    registration

      let f be Lipschitzian PartFunc of REAL , REAL ;

      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 that

             A4: x1 in ( dom (p (#) f)) and

             A5: x2 in ( dom (p (#) f));

            

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

             |.(((p (#) f) . x1) - ((p (#) f) . x2)).| = |.((p * (f . x1)) - ((p (#) f) . x2)).| by A4, VALUED_1:def 5

            .= |.( 0 qua Nat - (p * (f . x2))).| by A3, A5, VALUED_1:def 5

            .= 0 by A3, ABSVALUE: 2;

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

          end;

          hence thesis;

        end;

          suppose p <> 0 ;

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

          then

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

          now

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

            

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

            thus 0 < g by A7;

            let x1, x2;

            assume that

             A9: x1 in ( dom (p (#) f)) and

             A10: x2 in ( dom (p (#) f));

            

             A11: |.(((p (#) f) . x1) - ((p (#) f) . x2)).| = |.((p * (f . x1)) - ((p (#) f) . x2)).| by A9, VALUED_1:def 5

            .= |.((p * (f . x1)) - (p * (f . x2))).| by A10, VALUED_1:def 5

            .= |.(p * ((f . x1) - (f . x2))).|

            .= ( |.p.| * |.((f . x1) - (f . x2)).|) by COMPLEX1: 65;

            x1 in ( dom f) & x2 in ( dom f) by A9, A10, VALUED_1:def 5;

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

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

          end;

          hence thesis;

        end;

      end;

    end

    theorem :: FCONT_1:37

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

    proof

      ((p (#) f) | X) = (p (#) (f | X)) by RFUNCT_1: 49;

      hence thesis;

    end;

    registration

      let f be Lipschitzian PartFunc of REAL , REAL ;

      cluster ( abs 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

          take s;

          thus 0 < s by A1;

          let x1, x2;

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

          then x1 in ( dom f) & x2 in ( dom f) by VALUED_1:def 11;

          then

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

           |.((( abs f) . x1) - (( abs f) . x2)).| = |.( |.(f . x1).| - (( abs f) . x2)).| by VALUED_1: 18

          .= |.( |.(f . x1).| - |.(f . x2).|).| by VALUED_1: 18;

          then |.((( abs f) . x1) - (( abs f) . x2)).| <= |.((f . x1) - (f . x2)).| by COMPLEX1: 64;

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

        end;

        hence thesis;

      end;

    end

    theorem :: FCONT_1:38

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

    proof

      assume

       A1: (f | X) is Lipschitzian;

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

      (( abs f) | X) = ( abs (f | X)) by RFUNCT_1: 46;

      hence thesis by A1;

    end;

    registration

      cluster constant -> Lipschitzian for PartFunc of REAL , REAL ;

      coherence

      proof

        let f be PartFunc of REAL , REAL such that

         A1: f is constant;

        now

          let x1, x2;

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

          then (f . x1) = (f . x2) by A1;

          then |.((f . x1) - (f . x2)).| = 0 by ABSVALUE: 2;

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

        end;

        hence thesis;

      end;

    end

    registration

      let Y;

      cluster ( id Y) -> Lipschitzian;

      coherence

      proof

        reconsider r = 1 as Real;

        ( id Y) is Lipschitzian

        proof

          take r;

          thus r > 0 ;

          let x1, x2;

          assume that

           A1: x1 in ( dom ( id Y)) and

           A2: x2 in ( dom ( id Y));

          

           A3: x2 in Y by A2;

          x1 in Y by A1;

          

          then |.((( id Y) . x1) - (( id Y) . x2)).| = |.(x1 - (( id Y) . x2)).| by FUNCT_1: 18

          .= (r * |.(x1 - x2).|) by A3, FUNCT_1: 18;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      ::$Notion-Name

      cluster Lipschitzian -> continuous for PartFunc of REAL , REAL ;

      coherence

      proof

        let f be PartFunc of REAL , REAL ;

        set X = ( dom f);

        assume f is Lipschitzian;

        then

        consider r 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 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 Th3;

        end;

        hence thesis;

      end;

    end

    theorem :: FCONT_1:39

    for f st (ex r st ( rng f) = {r}) holds f is continuous

    proof

      let f;

      given r 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

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

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

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

        then |.((f . x1) - (f . x2)).| = 0 by A4, ABSVALUE: 2;

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

      end;

      then f is Lipschitzian;

      hence thesis;

    end;

    theorem :: FCONT_1:40

    for f st (for x0 st x0 in ( dom f) holds (f . x0) = x0) holds f is continuous

    proof

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

      hence thesis;

    end;

    theorem :: FCONT_1:41

    

     Th41: (for x0 st x0 in X holds (f . x0) = ((r * x0) + p)) implies (f | X) is continuous

    proof

      assume

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

       A2:

      now

        let x1, x2;

        assume that

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

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

        x2 in X by A4;

        then

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

        

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

        x1 in X by A3;

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

        

        then |.((f . x1) - (f . x2)).| = |.(r * (x1 - x2)).| by A5

        .= ( |.r.| * |.(x1 - x2).|) by COMPLEX1: 65;

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

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

      end;

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

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

      hence thesis;

    end;

    theorem :: FCONT_1:42

    

     Th42: (for x0 st x0 in ( dom f) holds (f . x0) = (x0 ^2 )) implies (f | ( dom f)) is continuous

    proof

      reconsider f1 = ( id ( dom f)) as PartFunc of REAL , REAL ;

      assume

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

       A2:

      now

        let x0 be object;

        assume

         A3: x0 in ( dom f);

        then

        reconsider x1 = x0 as Real;

        

        thus (f . x0) = (x1 ^2 ) by A1, A3

        .= ((f1 . x1) * x1) by A3, FUNCT_1: 18

        .= ((f1 . x0) * (f1 . x0)) by A3, FUNCT_1: 18;

      end;

      (( dom f1) /\ ( dom f1)) = ( dom f);

      then f = (f1 (#) f1) by A2, VALUED_1:def 4;

      hence thesis;

    end;

    theorem :: FCONT_1:43

    X c= ( dom f) & (for x0 st x0 in X holds (f . x0) = (x0 ^2 )) implies (f | X) is continuous

    proof

      assume that

       A1: X c= ( dom f) and

       A2: for x0 st x0 in X holds (f . x0) = (x0 ^2 );

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

        then (f . x0) = (x0 ^2 ) by A2;

        hence ((f | X) . x0) = (x0 ^2 ) by A4, FUNCT_1: 47;

      end;

      then ((f | X) | X) is continuous by A3, Th42;

      hence thesis;

    end;

    theorem :: FCONT_1:44

    

     Th44: (for x0 st x0 in ( dom f) holds (f . x0) = |.x0.|) implies f is continuous

    proof

      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 COMPLEX1: 64;

      end;

      then f is Lipschitzian;

      hence thesis;

    end;

    theorem :: FCONT_1:45

    (for x0 st x0 in X holds (f . x0) = |.x0.|) implies (f | X) is continuous

    proof

      assume that

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

      now

        let x0;

        assume

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

        then (f . x0) = |.x0.| by A1;

        hence ((f | X) . x0) = |.x0.| by A2, FUNCT_1: 47;

      end;

      hence thesis by Th44;

    end;

    theorem :: FCONT_1:46

    

     Th46: (f | X) is monotone & (ex p, g st p <= g & (f .: X) = [.p, g.]) implies (f | X) is continuous

    proof

      assume

       A1: (f | X) is monotone;

      given p, g such that

       A2: p <= g and

       A3: (f .: X) = [.p, g.];

      reconsider p, g as Real;

      now

        per cases by A2, XXREAL_0: 1;

          suppose p = g;

          then (f .: X) = {p} by A3, XXREAL_1: 17;

          then ( rng (f | X)) = {p} by RELAT_1: 115;

          then (f | X) is constant;

          hence thesis;

        end;

          suppose

           A4: p < g;

          now

            per cases by A1, RFUNCT_2:def 5;

              suppose (f | X) is non-decreasing;

              then

               A5: ((f | X) | X) is non-decreasing;

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

              proof

                

                 A6: [.p, g.] = ( ].p, g.[ \/ {p, g}) by A2, XXREAL_1: 128;

                let x0;

                

                 A7: ((f | X) .: X) = (f .: X) by RELAT_1: 129;

                assume

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

                

                 A9: ((f | X) . x0) in ((f | X) .: X) by A8, FUNCT_1:def 6;

                reconsider x0 as Real;

                ((f | X) . x0) in [.p, g.] by A3, A9, RELAT_1: 129;

                then

                 A10: ((f | X) . x0) in ].p, g.[ or ((f | X) . x0) in {p, g} by A6, XBOOLE_0:def 3;

                now

                  let N1 be Neighbourhood of ((f | X) . x0);

                  now

                    per cases by A10, TARSKI:def 2;

                      suppose ((f | X) . x0) in ].p, g.[;

                      then

                      consider N2 be Neighbourhood of ((f | X) . x0) such that

                       A11: N2 c= ].p, g.[ by RCOMP_1: 18;

                      

                       A12: ].p, g.[ c= [.p, g.] by XXREAL_1: 25;

                      consider N3 be Neighbourhood of ((f | X) . x0) such that

                       A13: N3 c= N1 and

                       A14: N3 c= N2 by RCOMP_1: 17;

                      consider r such that

                       A15: r > 0 and

                       A16: N3 = ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by RCOMP_1:def 6;

                      reconsider r as Real;

                      

                       A17: (((f | X) . x0) + (r / 2)) < ((((f | X) . x0) + (r / 2)) + (r / 2)) by A15, XREAL_1: 29, XREAL_1: 215;

                      set M2 = (((f | X) . x0) + (r / 2));

                      

                       A18: ((f | X) . x0) < (((f | X) . x0) + (r / 2)) by A15, XREAL_1: 29, XREAL_1: 215;

                      

                       A19: ((f | X) . x0) < (((f | X) . x0) + r) by A15, XREAL_1: 29;

                      then (((f | X) . x0) - r) < ((((f | X) . x0) + r) - r) by XREAL_1: 9;

                      then (((f | X) . x0) - r) < (((f | X) . x0) + (r / 2)) by A18, XXREAL_0: 2;

                      then (((f | X) . x0) + (r / 2)) in { s : (((f | X) . x0) - r) < s & s < (((f | X) . x0) + r) } by A17;

                      then

                       A20: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by RCOMP_1:def 2;

                      then M2 in N2 by A14, A16;

                      then M2 in ].p, g.[ by A11;

                      then

                      consider x2 be Element of REAL such that

                       A21: x2 in ( dom (f | X)) & x2 in X and

                       A22: M2 = ((f | X) . x2) by A3, A7, A12, PARTFUN2: 59;

                      

                       A23: ].p, g.[ c= [.p, g.] by XXREAL_1: 25;

                      set M1 = (((f | X) . x0) - (r / 2));

                      

                       A24: (((f | X) . x0) - r) < ((((f | X) . x0) - r) + (r / 2)) by A15, XREAL_1: 29, XREAL_1: 215;

                      (((f | X) . x0) - (r / 2)) < ((f | X) . x0) by A18, XREAL_1: 19;

                      then (((f | X) . x0) - (r / 2)) < (((f | X) . x0) + r) by A19, XXREAL_0: 2;

                      then (((f | X) . x0) - (r / 2)) in { s : (((f | X) . x0) - r) < s & s < (((f | X) . x0) + r) } by A24;

                      then

                       A25: M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by RCOMP_1:def 2;

                      then M1 in N2 by A14, A16;

                      then M1 in ].p, g.[ by A11;

                      then

                      consider x1 be Element of REAL such that

                       A26: x1 in ( dom (f | X)) & x1 in X and

                       A27: M1 = ((f | X) . x1) by A3, A7, A23, PARTFUN2: 59;

                      

                       A28: ((f | X) . x0) < (((f | X) . x0) + (r / 2)) by A15, XREAL_1: 29, XREAL_1: 215;

                      then

                       A29: M1 < ((f | X) . x0) by XREAL_1: 19;

                       A30:

                      now

                        assume

                         A31: x0 < x1;

                        x0 in (X /\ ( dom (f | X))) & x1 in (X /\ ( dom (f | X))) by A8, A26, XBOOLE_0:def 4;

                        hence contradiction by A5, A27, A29, A31, RFUNCT_2: 22;

                      end;

                      

                       A32: M2 > ((f | X) . x0) by A15, XREAL_1: 29, XREAL_1: 215;

                       A33:

                      now

                        assume

                         A34: x2 < x0;

                        x0 in (X /\ ( dom (f | X))) & x2 in (X /\ ( dom (f | X))) by A8, A21, XBOOLE_0:def 4;

                        hence contradiction by A5, A22, A32, A34, RFUNCT_2: 22;

                      end;

                      x0 <> x2 by A15, A22, XREAL_1: 29, XREAL_1: 215;

                      then x0 < x2 by A33, XXREAL_0: 1;

                      then

                       A35: (x2 - x0) > 0 by XREAL_1: 50;

                      set R = ( min ((x0 - x1),(x2 - x0)));

                      

                       A36: R <= (x2 - x0) by XXREAL_0: 17;

                      x1 <> x0 by A27, A28, XREAL_1: 19;

                      then x1 < x0 by A30, XXREAL_0: 1;

                      then (x0 - x1) > 0 by XREAL_1: 50;

                      then R > 0 by A35, XXREAL_0: 15;

                      then

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

                      take N;

                      let x be Real;

                      assume that

                       A37: x in ( dom (f | X)) and

                       A38: x in N;

                      

                       A39: x in (X /\ ( dom (f | X))) by A37, XBOOLE_1: 28;

                      x in { s : (x0 - R) < s & s < (x0 + R) } by A38, RCOMP_1:def 2;

                      then

                       A40: ex s st s = x & (x0 - R) < s & s < (x0 + R);

                      then x0 < (R + x) by XREAL_1: 19;

                      then

                       A41: (x0 - x) < ((R + x) - x) by XREAL_1: 9;

                      R <= (x0 - x1) by XXREAL_0: 17;

                      then (x0 - x) < (x0 - x1) by A41, XXREAL_0: 2;

                      then ( - (x0 - x)) > ( - (x0 - x1)) by XREAL_1: 24;

                      then

                       A42: ((x - x0) + x0) > ((x1 - x0) + x0) by XREAL_1: 6;

                      x1 in (X /\ ( dom (f | X))) by A26, XBOOLE_0:def 4;

                      then

                       A43: ((f | X) . x1) <= ((f | X) . x) by A5, A42, A39, RFUNCT_2: 22;

                      (x - x0) < R by A40, XREAL_1: 19;

                      then (x - x0) < (x2 - x0) by A36, XXREAL_0: 2;

                      then

                       A44: ((x - x0) + x0) < ((x2 - x0) + x0) by XREAL_1: 6;

                      x2 in (X /\ ( dom (f | X))) by A21, XBOOLE_0:def 4;

                      then ((f | X) . x) <= ((f | X) . x2) by A5, A44, A39, RFUNCT_2: 22;

                      then ((f | X) . x) in { s : M1 <= s & s <= M2 } by A27, A22, A43;

                      then

                       A45: ((f | X) . x) in [.M1, M2.] by RCOMP_1:def 1;

                       [.M1, M2.] c= ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A25, A20, XXREAL_2:def 12;

                      then ((f | X) . x) in N3 by A16, A45;

                      hence ((f | X) . x) in N1 by A13;

                    end;

                      suppose

                       A46: ((f | X) . x0) = p;

                      then

                      consider r such that

                       A47: r > 0 and

                       A48: N1 = ].(p - r), (p + r).[ by RCOMP_1:def 6;

                      reconsider r as Real;

                      set R = (( min (r,(g - p))) / 2);

                      (g - p) > 0 by A4, XREAL_1: 50;

                      then

                       A49: ( min (r,(g - p))) > 0 by A47, XXREAL_0: 15;

                      then

                       A50: R < ( min (r,(g - p))) by XREAL_1: 216;

                      ( min (r,(g - p))) <= r by XXREAL_0: 17;

                      then

                       A51: R < r by A50, XXREAL_0: 2;

                      then

                       A52: (p + R) < (p + r) by XREAL_1: 6;

                      

                       A53: (p - R) < p by A49, XREAL_1: 44, XREAL_1: 215;

                      ( - r) < ( - R) by A51, XREAL_1: 24;

                      then

                       A54: (p + ( - r)) < (p + ( - R)) by XREAL_1: 6;

                      p < (p + r) by A47, XREAL_1: 29;

                      then (p - R) < (p + r) by A53, XXREAL_0: 2;

                      then (p - R) in { s : (p - r) < s & s < (p + r) } by A54;

                      then

                       A55: (p - R) in ].(p - r), (p + r).[ by RCOMP_1:def 2;

                      

                       A56: ].p, g.[ c= [.p, g.] by XXREAL_1: 25;

                      

                       A57: p < (p + R) by A49, XREAL_1: 29, XREAL_1: 215;

                      ( min (r,(g - p))) <= (g - p) by XXREAL_0: 17;

                      then R < (g - p) by A50, XXREAL_0: 2;

                      then (p + R) < g by XREAL_1: 20;

                      then (p + R) in { s : p < s & s < g } by A57;

                      then (p + R) in ].p, g.[ by RCOMP_1:def 2;

                      then

                      consider x1 be Element of REAL such that

                       A58: x1 in ( dom (f | X)) & x1 in X and

                       A59: (p + R) = ((f | X) . x1) by A3, A7, A56, PARTFUN2: 59;

                      

                       A60: x1 in (X /\ ( dom (f | X))) by A58, XBOOLE_0:def 4;

                      now

                        assume

                         A61: x1 < x0;

                        x0 in (X /\ ( dom (f | X))) & x1 in (X /\ ( dom (f | X))) by A8, A58, XBOOLE_0:def 4;

                        hence contradiction by A5, A46, A57, A59, A61, RFUNCT_2: 22;

                      end;

                      then x0 < x1 by A46, A57, A59, XXREAL_0: 1;

                      then

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

                      take N;

                      let x be Real such that

                       A62: x in ( dom (f | X)) and

                       A63: x in N;

                      x in { s : (x0 - (x1 - x0)) < s & s < (x0 + (x1 - x0)) } by A63, RCOMP_1:def 2;

                      then

                       A64: ex s st s = x & (x0 - (x1 - x0)) < s & s < (x0 + (x1 - x0));

                      ((f | X) . x) in [.p, g.] by A3, A7, A62, FUNCT_1:def 6;

                      then ((f | X) . x) in { s : p <= s & s <= g } by RCOMP_1:def 1;

                      then ex s st s = ((f | X) . x) & p <= s & s <= g;

                      then

                       A65: (p - R) <= ((f | X) . x) by A53, XXREAL_0: 2;

                      x in (X /\ ( dom (f | X))) by A62, XBOOLE_0:def 4;

                      then ((f | X) . x) <= (p + R) by A5, A59, A60, A64, RFUNCT_2: 22;

                      then ((f | X) . x) in { s : (p - R) <= s & s <= (p + R) } by A65;

                      then

                       A66: ((f | X) . x) in [.(p - R), (p + R).] by RCOMP_1:def 1;

                      (p - r) < p by A47, XREAL_1: 44;

                      then (p - r) < (p + R) by A57, XXREAL_0: 2;

                      then (p + R) in { s : (p - r) < s & s < (p + r) } by A52;

                      then (p + R) in ].(p - r), (p + r).[ by RCOMP_1:def 2;

                      then [.(p - R), (p + R).] c= N1 by A48, A55, XXREAL_2:def 12;

                      hence ((f | X) . x) in N1 by A66;

                    end;

                      suppose

                       A67: ((f | X) . x0) = g;

                      

                       A68: ].p, g.[ c= [.p, g.] by XXREAL_1: 25;

                      consider r such that

                       A69: r > 0 and

                       A70: N1 = ].(g - r), (g + r).[ by A67, RCOMP_1:def 6;

                      reconsider r as Real;

                      set R = (( min (r,(g - p))) / 2);

                      (g - p) > 0 by A4, XREAL_1: 50;

                      then

                       A71: ( min (r,(g - p))) > 0 by A69, XXREAL_0: 15;

                      then

                       A72: R < ( min (r,(g - p))) by XREAL_1: 216;

                      

                       A73: (g - R) < g by A71, XREAL_1: 44, XREAL_1: 215;

                      ( min (r,(g - p))) <= (g - p) by XXREAL_0: 17;

                      then R < (g - p) by A72, XXREAL_0: 2;

                      then (R + p) < g by XREAL_1: 20;

                      then (g - R) > p by XREAL_1: 20;

                      then (g - R) in { s : p < s & s < g } by A73;

                      then (g - R) in ].p, g.[ by RCOMP_1:def 2;

                      then

                      consider x1 be Element of REAL such that

                       A74: x1 in ( dom (f | X)) & x1 in X and

                       A75: (g - R) = ((f | X) . x1) by A3, A7, A68, PARTFUN2: 59;

                       A76:

                      now

                        assume

                         A77: x0 < x1;

                        x0 in (X /\ ( dom (f | X))) & x1 in (X /\ ( dom (f | X))) by A8, A74, XBOOLE_0:def 4;

                        hence contradiction by A5, A67, A73, A75, A77, RFUNCT_2: 22;

                      end;

                      ( min (r,(g - p))) <= r by XXREAL_0: 17;

                      then

                       A78: R < r by A72, XXREAL_0: 2;

                      then

                       A79: (g + R) < (g + r) by XREAL_1: 6;

                      ( - r) < ( - R) by A78, XREAL_1: 24;

                      then

                       A80: (g + ( - r)) < (g + ( - R)) by XREAL_1: 6;

                      g < (g + r) by A69, XREAL_1: 29;

                      then (g - R) < (g + r) by A73, XXREAL_0: 2;

                      then (g - R) in { s : (g - r) < s & s < (g + r) } by A80;

                      then

                       A81: (g - R) in ].(g - r), (g + r).[ by RCOMP_1:def 2;

                      

                       A82: x1 in (X /\ ( dom (f | X))) by A74, XBOOLE_0:def 4;

                      

                       A83: g < (g + R) by A71, XREAL_1: 29, XREAL_1: 215;

                      x1 <> x0 by A67, A71, A75, XREAL_1: 44, XREAL_1: 215;

                      then x1 < x0 by A76, XXREAL_0: 1;

                      then

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

                      take N;

                      let x be Real such that

                       A84: x in ( dom (f | X)) and

                       A85: x in N;

                      x in { s : (x0 - (x0 - x1)) < s & s < (x0 + (x0 - x1)) } by A85, RCOMP_1:def 2;

                      then

                       A86: ex s st s = x & (x0 - (x0 - x1)) < s & s < (x0 + (x0 - x1));

                      ((f | X) . x) in [.p, g.] by A3, A7, A84, FUNCT_1:def 6;

                      then ((f | X) . x) in { s : p <= s & s <= g } by RCOMP_1:def 1;

                      then ex s st s = ((f | X) . x) & p <= s & s <= g;

                      then

                       A87: ((f | X) . x) <= (g + R) by A83, XXREAL_0: 2;

                      x in (X /\ ( dom (f | X))) by A84, XBOOLE_0:def 4;

                      then (g - R) <= ((f | X) . x) by A5, A75, A82, A86, RFUNCT_2: 22;

                      then ((f | X) . x) in { s : (g - R) <= s & s <= (g + R) } by A87;

                      then

                       A88: ((f | X) . x) in [.(g - R), (g + R).] by RCOMP_1:def 1;

                      (g - r) < g by A69, XREAL_1: 44;

                      then (g - r) < (g + R) by A83, XXREAL_0: 2;

                      then (g + R) in { s : (g - r) < s & s < (g + r) } by A79;

                      then (g + R) in ].(g - r), (g + r).[ by RCOMP_1:def 2;

                      then [.(g - R), (g + R).] c= N1 by A70, A81, XXREAL_2:def 12;

                      hence ((f | X) . x) in N1 by A88;

                    end;

                  end;

                  then

                  consider N be Neighbourhood of x0 such that

                   A89: for x1 be Real st x1 in ( dom (f | X)) & x1 in N holds ((f | X) . x1) in N1;

                  take N;

                  thus for x1 be Real st x1 in ( dom (f | X)) & x1 in N holds ((f | X) . x1) in N1 by A89;

                end;

                hence thesis by Th4;

              end;

              hence thesis;

            end;

              suppose (f | X) is non-increasing;

              then

               A90: ((f | X) | X) is non-increasing;

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

              proof

                

                 A91: [.p, g.] = ( ].p, g.[ \/ {p, g}) by A2, XXREAL_1: 128;

                let x0;

                

                 A92: ((f | X) .: X) = (f .: X) by RELAT_1: 129;

                assume

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

                

                 A94: ((f | X) . x0) in ((f | X) .: X) by A93, FUNCT_1:def 6;

                reconsider x0 as Real;

                ((f | X) . x0) in [.p, g.] by A3, A94, RELAT_1: 129;

                then

                 A95: ((f | X) . x0) in ].p, g.[ or ((f | X) . x0) in {p, g} by A91, XBOOLE_0:def 3;

                now

                  let N1 be Neighbourhood of ((f | X) . x0);

                  now

                    per cases by A95, TARSKI:def 2;

                      suppose ((f | X) . x0) in ].p, g.[;

                      then

                      consider N2 be Neighbourhood of ((f | X) . x0) such that

                       A96: N2 c= ].p, g.[ by RCOMP_1: 18;

                      

                       A97: ].p, g.[ c= [.p, g.] by XXREAL_1: 25;

                      consider N3 be Neighbourhood of ((f | X) . x0) such that

                       A98: N3 c= N1 and

                       A99: N3 c= N2 by RCOMP_1: 17;

                      consider r such that

                       A100: r > 0 and

                       A101: N3 = ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by RCOMP_1:def 6;

                      reconsider r as Real;

                      

                       A102: (((f | X) . x0) + (r / 2)) < ((((f | X) . x0) + (r / 2)) + (r / 2)) by A100, XREAL_1: 29, XREAL_1: 215;

                      set M2 = (((f | X) . x0) + (r / 2));

                      

                       A103: ((f | X) . x0) < (((f | X) . x0) + (r / 2)) by A100, XREAL_1: 29, XREAL_1: 215;

                      

                       A104: ((f | X) . x0) < (((f | X) . x0) + r) by A100, XREAL_1: 29;

                      then (((f | X) . x0) - r) < ((((f | X) . x0) + r) - r) by XREAL_1: 9;

                      then (((f | X) . x0) - r) < (((f | X) . x0) + (r / 2)) by A103, XXREAL_0: 2;

                      then (((f | X) . x0) + (r / 2)) in { s : (((f | X) . x0) - r) < s & s < (((f | X) . x0) + r) } by A102;

                      then

                       A105: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by RCOMP_1:def 2;

                      then M2 in N2 by A99, A101;

                      then M2 in ].p, g.[ by A96;

                      then

                      consider x2 be Element of REAL such that

                       A106: x2 in ( dom (f | X)) & x2 in X and

                       A107: M2 = ((f | X) . x2) by A3, A92, A97, PARTFUN2: 59;

                      

                       A108: ].p, g.[ c= [.p, g.] by XXREAL_1: 25;

                      set M1 = (((f | X) . x0) - (r / 2));

                      

                       A109: (((f | X) . x0) - r) < ((((f | X) . x0) - r) + (r / 2)) by A100, XREAL_1: 29, XREAL_1: 215;

                      (((f | X) . x0) - (r / 2)) < ((f | X) . x0) by A103, XREAL_1: 19;

                      then (((f | X) . x0) - (r / 2)) < (((f | X) . x0) + r) by A104, XXREAL_0: 2;

                      then (((f | X) . x0) - (r / 2)) in { s : (((f | X) . x0) - r) < s & s < (((f | X) . x0) + r) } by A109;

                      then

                       A110: M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by RCOMP_1:def 2;

                      then M1 in N2 by A99, A101;

                      then M1 in ].p, g.[ by A96;

                      then

                      consider x1 be Element of REAL such that

                       A111: x1 in ( dom (f | X)) & x1 in X and

                       A112: M1 = ((f | X) . x1) by A3, A92, A108, PARTFUN2: 59;

                      

                       A113: ((f | X) . x0) < (((f | X) . x0) + (r / 2)) by A100, XREAL_1: 29, XREAL_1: 215;

                      then

                       A114: M1 < ((f | X) . x0) by XREAL_1: 19;

                       A115:

                      now

                        assume

                         A116: x0 > x1;

                        x0 in (X /\ ( dom (f | X))) & x1 in (X /\ ( dom (f | X))) by A93, A111, XBOOLE_0:def 4;

                        hence contradiction by A90, A112, A114, A116, RFUNCT_2: 23;

                      end;

                      

                       A117: M2 > ((f | X) . x0) by A100, XREAL_1: 29, XREAL_1: 215;

                       A118:

                      now

                        assume

                         A119: x2 > x0;

                        x0 in (X /\ ( dom (f | X))) & x2 in (X /\ ( dom (f | X))) by A93, A106, XBOOLE_0:def 4;

                        hence contradiction by A90, A107, A117, A119, RFUNCT_2: 23;

                      end;

                      x0 <> x2 by A100, A107, XREAL_1: 29, XREAL_1: 215;

                      then x0 > x2 by A118, XXREAL_0: 1;

                      then

                       A120: (x0 - x2) > 0 by XREAL_1: 50;

                      set R = ( min ((x1 - x0),(x0 - x2)));

                      

                       A121: R <= (x1 - x0) by XXREAL_0: 17;

                      x1 <> x0 by A112, A113, XREAL_1: 19;

                      then x1 > x0 by A115, XXREAL_0: 1;

                      then (x1 - x0) > 0 by XREAL_1: 50;

                      then R > 0 by A120, XXREAL_0: 15;

                      then

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

                      take N;

                      let x be Real;

                      assume that

                       A122: x in ( dom (f | X)) and

                       A123: x in N;

                      

                       A124: x in (X /\ ( dom (f | X))) by A122, XBOOLE_1: 28;

                      x in { s : (x0 - R) < s & s < (x0 + R) } by A123, RCOMP_1:def 2;

                      then

                       A125: ex s st s = x & (x0 - R) < s & s < (x0 + R);

                      then x0 < (R + x) by XREAL_1: 19;

                      then

                       A126: (x0 - x) < ((R + x) - x) by XREAL_1: 9;

                      (x - x0) < R by A125, XREAL_1: 19;

                      then (x - x0) < (x1 - x0) by A121, XXREAL_0: 2;

                      then

                       A127: ((x - x0) + x0) < ((x1 - x0) + x0) by XREAL_1: 6;

                      x1 in (X /\ ( dom (f | X))) by A111, XBOOLE_0:def 4;

                      then

                       A128: ((f | X) . x1) <= ((f | X) . x) by A90, A127, A124, RFUNCT_2: 23;

                      R <= (x0 - x2) by XXREAL_0: 17;

                      then (x0 - x) < (x0 - x2) by A126, XXREAL_0: 2;

                      then ( - (x0 - x)) > ( - (x0 - x2)) by XREAL_1: 24;

                      then

                       A129: ((x - x0) + x0) > ((x2 - x0) + x0) by XREAL_1: 6;

                      x2 in (X /\ ( dom (f | X))) by A106, XBOOLE_0:def 4;

                      then ((f | X) . x) <= ((f | X) . x2) by A90, A129, A124, RFUNCT_2: 23;

                      then ((f | X) . x) in { s : M1 <= s & s <= M2 } by A112, A107, A128;

                      then

                       A130: ((f | X) . x) in [.M1, M2.] by RCOMP_1:def 1;

                       [.M1, M2.] c= ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A110, A105, XXREAL_2:def 12;

                      then ((f | X) . x) in N3 by A101, A130;

                      hence ((f | X) . x) in N1 by A98;

                    end;

                      suppose

                       A131: ((f | X) . x0) = p;

                      then

                      consider r such that

                       A132: r > 0 and

                       A133: N1 = ].(p - r), (p + r).[ by RCOMP_1:def 6;

                      reconsider r as Real;

                      set R = (( min (r,(g - p))) / 2);

                      (g - p) > 0 by A4, XREAL_1: 50;

                      then

                       A134: ( min (r,(g - p))) > 0 by A132, XXREAL_0: 15;

                      then

                       A135: R < ( min (r,(g - p))) by XREAL_1: 216;

                      ( min (r,(g - p))) <= r by XXREAL_0: 17;

                      then

                       A136: R < r by A135, XXREAL_0: 2;

                      then

                       A137: (p + R) < (p + r) by XREAL_1: 6;

                      

                       A138: (p - R) < p by A134, XREAL_1: 44, XREAL_1: 215;

                      ( - r) < ( - R) by A136, XREAL_1: 24;

                      then

                       A139: (p + ( - r)) < (p + ( - R)) by XREAL_1: 6;

                      p < (p + r) by A132, XREAL_1: 29;

                      then (p - R) < (p + r) by A138, XXREAL_0: 2;

                      then (p - R) in { s : (p - r) < s & s < (p + r) } by A139;

                      then

                       A140: (p - R) in ].(p - r), (p + r).[ by RCOMP_1:def 2;

                      

                       A141: ].p, g.[ c= [.p, g.] by XXREAL_1: 25;

                      

                       A142: p < (p + R) by A134, XREAL_1: 29, XREAL_1: 215;

                      ( min (r,(g - p))) <= (g - p) by XXREAL_0: 17;

                      then R < (g - p) by A135, XXREAL_0: 2;

                      then (p + R) < g by XREAL_1: 20;

                      then (p + R) in { s : p < s & s < g } by A142;

                      then (p + R) in ].p, g.[ by RCOMP_1:def 2;

                      then

                      consider x1 be Element of REAL such that

                       A143: x1 in ( dom (f | X)) & x1 in X and

                       A144: (p + R) = ((f | X) . x1) by A3, A92, A141, PARTFUN2: 59;

                      

                       A145: x1 in (X /\ ( dom (f | X))) by A143, XBOOLE_0:def 4;

                      now

                        assume

                         A146: x1 > x0;

                        x0 in (X /\ ( dom (f | X))) & x1 in (X /\ ( dom (f | X))) by A93, A143, XBOOLE_0:def 4;

                        hence contradiction by A90, A131, A142, A144, A146, RFUNCT_2: 23;

                      end;

                      then x0 > x1 by A131, A142, A144, XXREAL_0: 1;

                      then

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

                      take N;

                      let x be Real such that

                       A147: x in ( dom (f | X)) and

                       A148: x in N;

                      x in { s : (x0 - (x0 - x1)) < s & s < (x0 + (x0 - x1)) } by A148, RCOMP_1:def 2;

                      then

                       A149: ex s st s = x & (x0 - (x0 - x1)) < s & s < (x0 + (x0 - x1));

                      ((f | X) . x) in [.p, g.] by A3, A92, A147, FUNCT_1:def 6;

                      then ((f | X) . x) in { s : p <= s & s <= g } by RCOMP_1:def 1;

                      then ex s st s = ((f | X) . x) & p <= s & s <= g;

                      then

                       A150: (p - R) <= ((f | X) . x) by A138, XXREAL_0: 2;

                      x in (X /\ ( dom (f | X))) by A147, XBOOLE_0:def 4;

                      then ((f | X) . x) <= (p + R) by A90, A144, A145, A149, RFUNCT_2: 23;

                      then ((f | X) . x) in { s : (p - R) <= s & s <= (p + R) } by A150;

                      then

                       A151: ((f | X) . x) in [.(p - R), (p + R).] by RCOMP_1:def 1;

                      (p - r) < p by A132, XREAL_1: 44;

                      then (p - r) < (p + R) by A142, XXREAL_0: 2;

                      then (p + R) in { s : (p - r) < s & s < (p + r) } by A137;

                      then (p + R) in ].(p - r), (p + r).[ by RCOMP_1:def 2;

                      then [.(p - R), (p + R).] c= N1 by A133, A140, XXREAL_2:def 12;

                      hence ((f | X) . x) in N1 by A151;

                    end;

                      suppose

                       A152: ((f | X) . x0) = g;

                      

                       A153: ].p, g.[ c= [.p, g.] by XXREAL_1: 25;

                      consider r such that

                       A154: r > 0 and

                       A155: N1 = ].(g - r), (g + r).[ by A152, RCOMP_1:def 6;

                      reconsider r as Real;

                      set R = (( min (r,(g - p))) / 2);

                      (g - p) > 0 by A4, XREAL_1: 50;

                      then

                       A156: ( min (r,(g - p))) > 0 by A154, XXREAL_0: 15;

                      then

                       A157: R < ( min (r,(g - p))) by XREAL_1: 216;

                      

                       A158: (g - R) < g by A156, XREAL_1: 44, XREAL_1: 215;

                      ( min (r,(g - p))) <= (g - p) by XXREAL_0: 17;

                      then R < (g - p) by A157, XXREAL_0: 2;

                      then (R + p) < g by XREAL_1: 20;

                      then (g - R) > p by XREAL_1: 20;

                      then (g - R) in { s : p < s & s < g } by A158;

                      then (g - R) in ].p, g.[ by RCOMP_1:def 2;

                      then

                      consider x1 be Element of REAL such that

                       A159: x1 in ( dom (f | X)) & x1 in X and

                       A160: (g - R) = ((f | X) . x1) by A3, A92, A153, PARTFUN2: 59;

                       A161:

                      now

                        assume

                         A162: x0 > x1;

                        x0 in (X /\ ( dom (f | X))) & x1 in (X /\ ( dom (f | X))) by A93, A159, XBOOLE_0:def 4;

                        hence contradiction by A90, A152, A158, A160, A162, RFUNCT_2: 23;

                      end;

                      ( min (r,(g - p))) <= r by XXREAL_0: 17;

                      then

                       A163: R < r by A157, XXREAL_0: 2;

                      then

                       A164: (g + R) < (g + r) by XREAL_1: 6;

                      ( - r) < ( - R) by A163, XREAL_1: 24;

                      then

                       A165: (g + ( - r)) < (g + ( - R)) by XREAL_1: 6;

                      g < (g + r) by A154, XREAL_1: 29;

                      then (g - R) < (g + r) by A158, XXREAL_0: 2;

                      then (g - R) in { s : (g - r) < s & s < (g + r) } by A165;

                      then

                       A166: (g - R) in ].(g - r), (g + r).[ by RCOMP_1:def 2;

                      

                       A167: x1 in (X /\ ( dom (f | X))) by A159, XBOOLE_0:def 4;

                      

                       A168: g < (g + R) by A156, XREAL_1: 29, XREAL_1: 215;

                      x1 <> x0 by A152, A156, A160, XREAL_1: 44, XREAL_1: 215;

                      then x1 > x0 by A161, XXREAL_0: 1;

                      then

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

                      take N;

                      let x be Real such that

                       A169: x in ( dom (f | X)) and

                       A170: x in N;

                      x in { s : (x0 - (x1 - x0)) < s & s < (x0 + (x1 - x0)) } by A170, RCOMP_1:def 2;

                      then

                       A171: ex s st s = x & (x0 - (x1 - x0)) < s & s < (x0 + (x1 - x0));

                      ((f | X) . x) in [.p, g.] by A3, A92, A169, FUNCT_1:def 6;

                      then ((f | X) . x) in { s : p <= s & s <= g } by RCOMP_1:def 1;

                      then ex s st s = ((f | X) . x) & p <= s & s <= g;

                      then

                       A172: ((f | X) . x) <= (g + R) by A168, XXREAL_0: 2;

                      x in (X /\ ( dom (f | X))) by A169, XBOOLE_0:def 4;

                      then (g - R) <= ((f | X) . x) by A90, A160, A167, A171, RFUNCT_2: 23;

                      then ((f | X) . x) in { s : (g - R) <= s & s <= (g + R) } by A172;

                      then

                       A173: ((f | X) . x) in [.(g - R), (g + R).] by RCOMP_1:def 1;

                      (g - r) < g by A154, XREAL_1: 44;

                      then (g - r) < (g + R) by A168, XXREAL_0: 2;

                      then (g + R) in { s : (g - r) < s & s < (g + r) } by A164;

                      then (g + R) in ].(g - r), (g + r).[ by RCOMP_1:def 2;

                      then [.(g - R), (g + R).] c= N1 by A155, A166, XXREAL_2:def 12;

                      hence ((f | X) . x) in N1 by A173;

                    end;

                  end;

                  then

                  consider N be Neighbourhood of x0 such that

                   A174: for x1 be Real st x1 in ( dom (f | X)) & x1 in N holds ((f | X) . x1) in N1;

                  take N;

                  thus for x1 st x1 in ( dom (f | X)) & x1 in N holds ((f | X) . x1) in N1 by A174;

                end;

                hence thesis by Th4;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_1:47

    for f be one-to-one PartFunc of REAL , REAL st p <= g & [.p, g.] c= ( dom f) & ((f | [.p, g.]) is increasing or (f | [.p, g.]) is decreasing) holds (((f | [.p, g.]) " ) | (f .: [.p, g.])) is continuous

    proof

      let f be one-to-one PartFunc of REAL , REAL ;

      assume that

       A1: p <= g and

       A2: [.p, g.] c= ( dom f) and

       A3: (f | [.p, g.]) is increasing or (f | [.p, g.]) is decreasing;

      reconsider p, g as Real;

      now

        per cases by A3;

          suppose

           A4: (f | [.p, g.]) is increasing;

          

           A5: (((f | [.p, g.]) " ) .: (f .: [.p, g.])) = (((f | [.p, g.]) " ) .: ( rng (f | [.p, g.]))) by RELAT_1: 115

          .= (((f | [.p, g.]) " ) .: ( dom ((f | [.p, g.]) " ))) by FUNCT_1: 33

          .= ( rng ((f | [.p, g.]) " )) by RELAT_1: 113

          .= ( dom (f | [.p, g.])) by FUNCT_1: 33

          .= (( dom f) /\ [.p, g.]) by RELAT_1: 61

          .= [.p, g.] by A2, XBOOLE_1: 28;

          (((f | [.p, g.]) " ) | (f .: [.p, g.])) is increasing by A4, RFUNCT_2: 51;

          hence thesis by A1, A5, Th46;

        end;

          suppose

           A6: (f | [.p, g.]) is decreasing;

          

           A7: (((f | [.p, g.]) " ) .: (f .: [.p, g.])) = (((f | [.p, g.]) " ) .: ( rng (f | [.p, g.]))) by RELAT_1: 115

          .= (((f | [.p, g.]) " ) .: ( dom ((f | [.p, g.]) " ))) by FUNCT_1: 33

          .= ( rng ((f | [.p, g.]) " )) by RELAT_1: 113

          .= ( dom (f | [.p, g.])) by FUNCT_1: 33

          .= (( dom f) /\ [.p, g.]) by RELAT_1: 61

          .= [.p, g.] by A2, XBOOLE_1: 28;

          (((f | [.p, g.]) " ) | (f .: [.p, g.])) is decreasing by A6, RFUNCT_2: 52;

          hence thesis by A1, A7, Th46;

        end;

      end;

      hence thesis;

    end;

    definition

      let a,b be Real;

      :: FCONT_1:def4

      func AffineMap (a,b) -> Function of REAL , REAL means

      : Def4: for x be Real holds (it . x) = ((a * x) + b);

      existence

      proof

        reconsider a9 = a, b9 = b as Element of REAL by XREAL_0:def 1;

        deffunc F( Real) = ( In (((a9 * $1) + b9), REAL ));

        consider f be Function of REAL , REAL such that

         A1: for x be Element of REAL holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        let x be Real;

        reconsider x9 = x as Element of REAL by XREAL_0:def 1;

        (f . x9) = F(x) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f,f9 be Function of REAL , REAL such that

         A2: for x be Real holds (f . x) = ((a * x) + b) and

         A3: for x be Real holds (f9 . x) = ((a * x) + b);

        now

          let x be Element of REAL ;

          

          thus (f . x) = ((a * x) + b) by A2

          .= (f9 . x) by A3;

        end;

        hence f = f9 by FUNCT_2: 63;

      end;

    end

    registration

      let a,b be Real;

      cluster ( AffineMap (a,b)) -> continuous;

      coherence

      proof

        set f = ( AffineMap (a,b));

        for x0 be Real st x0 in REAL holds (f . x0) = ((a * x0) + b) by Def4;

        then REAL = ( dom f) & (( AffineMap (a,b)) | REAL ) is continuous by Th41, FUNCT_2:def 1;

        hence thesis;

      end;

    end

    registration

      cluster continuous for Function of REAL , REAL ;

      existence

      proof

        take ( AffineMap (1,1));

        thus thesis;

      end;

    end

    theorem :: FCONT_1:48

    

     Th48: for a,b be Real holds (( AffineMap (a,b)) . 0 ) = b

    proof

      let a,b be Real;

      

      thus (( AffineMap (a,b)) . 0 ) = ((a * 0 ) + b) by Def4

      .= b;

    end;

    theorem :: FCONT_1:49

    

     Th49: for a,b be Real holds (( AffineMap (a,b)) . 1) = (a + b)

    proof

      let a,b be Real;

      

      thus (( AffineMap (a,b)) . 1) = ((a * 1) + b) by Def4

      .= (a + b);

    end;

    theorem :: FCONT_1:50

    

     Th50: for a,b be Real st a <> 0 holds ( AffineMap (a,b)) is one-to-one

    proof

      let a,b be Real such that

       A1: a <> 0 ;

      let x1,x2 be object;

      set f = ( AffineMap (a,b));

      assume x1 in ( dom f);

      then

      reconsider r1 = x1 as Real;

      assume x2 in ( dom f);

      then

      reconsider r2 = x2 as Real;

      assume (f . x1) = (f . x2);

      

      then ((a * r1) + b) = (f . x2) by Def4

      .= ((a * r2) + b) by Def4;

      hence thesis by A1, XCMPLX_1: 5;

    end;

    theorem :: FCONT_1:51

    for a,b,x,y be Real st a > 0 & x < y holds (( AffineMap (a,b)) . x) < (( AffineMap (a,b)) . y)

    proof

      let a,b,x,y be Real;

      assume a > 0 & x < y;

      then

       A1: (a * x) < (a * y) by XREAL_1: 68;

      (( AffineMap (a,b)) . x) = ((a * x) + b) & (( AffineMap (a,b)) . y) = ((a * y) + b) by Def4;

      hence thesis by A1, XREAL_1: 8;

    end;

    theorem :: FCONT_1:52

    for a,b,x,y be Real st a < 0 & x < y holds (( AffineMap (a,b)) . x) > (( AffineMap (a,b)) . y)

    proof

      let a,b,x,y be Real;

      assume a < 0 & x < y;

      then

       A1: (a * x) > (a * y) by XREAL_1: 69;

      (( AffineMap (a,b)) . x) = ((a * x) + b) & (( AffineMap (a,b)) . y) = ((a * y) + b) by Def4;

      hence thesis by A1, XREAL_1: 8;

    end;

    theorem :: FCONT_1:53

    

     Th53: for a,b,x,y be Real st a >= 0 & x <= y holds (( AffineMap (a,b)) . x) <= (( AffineMap (a,b)) . y)

    proof

      let a,b,x,y be Real;

      assume a >= 0 & x <= y;

      then

       A1: (a * x) <= (a * y) by XREAL_1: 64;

      (( AffineMap (a,b)) . x) = ((a * x) + b) & (( AffineMap (a,b)) . y) = ((a * y) + b) by Def4;

      hence thesis by A1, XREAL_1: 7;

    end;

    theorem :: FCONT_1:54

    for a,b,x,y be Real st a <= 0 & x <= y holds (( AffineMap (a,b)) . x) >= (( AffineMap (a,b)) . y)

    proof

      let a,b,x,y be Real;

      assume a <= 0 & x <= y;

      then

       A1: (a * x) >= (a * y) by XREAL_1: 65;

      (( AffineMap (a,b)) . x) = ((a * x) + b) & (( AffineMap (a,b)) . y) = ((a * y) + b) by Def4;

      hence thesis by A1, XREAL_1: 7;

    end;

    theorem :: FCONT_1:55

    

     Th55: for a,b be Real st a <> 0 holds ( rng ( AffineMap (a,b))) = REAL

    proof

      let a,b be Real such that

       A1: a <> 0 ;

      thus ( rng ( AffineMap (a,b))) c= REAL ;

      let e be object;

      assume e in REAL ;

      then

      reconsider r = e as Element of REAL ;

      reconsider s = ((r - b) / a) as Element of REAL by XREAL_0:def 1;

      (( AffineMap (a,b)) . s) = ((a * s) + b) by Def4

      .= ((r - b) + b) by A1, XCMPLX_1: 87

      .= r;

      then r in ( rng ( AffineMap (a,b))) by FUNCT_2: 4;

      hence thesis;

    end;

    theorem :: FCONT_1:56

    for a,b be Real st a <> 0 holds (( AffineMap (a,b)) qua Function " ) = ( AffineMap ((a " ),( - (b / a))))

    proof

      let a,b be Real such that

       A1: a <> 0 ;

      for x be Element of REAL holds ((( AffineMap ((a " ),( - (b / a)))) * ( AffineMap (a,b))) . x) = (( id REAL ) . x)

      proof

        let x be Element of REAL ;

        

        thus ((( AffineMap ((a " ),( - (b / a)))) * ( AffineMap (a,b))) . x) = (( AffineMap ((a " ),( - (b / a)))) . (( AffineMap (a,b)) . x)) by FUNCT_2: 15

        .= (( AffineMap ((a " ),( - (b / a)))) . ((a * x) + b)) by Def4

        .= (((a " ) * ((a * x) + b)) + ( - (b / a))) by Def4

        .= (((((a " ) * a) * x) + ((a " ) * b)) + ( - (b / a)))

        .= (((1 * x) + ((a " ) * b)) + ( - (b / a))) by A1, XCMPLX_0:def 7

        .= ((x + ((a " ) * b)) - (b / a))

        .= ((x + (b / a)) - (b / a)) by XCMPLX_0:def 9

        .= (( id REAL ) . x);

      end;

      then

       A2: (( AffineMap ((a " ),( - (b / a)))) * ( AffineMap (a,b))) = ( id REAL ) by FUNCT_2: 63;

      ( rng ( AffineMap (a,b))) = REAL by A1, Th55;

      hence thesis by A1, A2, Th50, FUNCT_2: 30;

    end;

    theorem :: FCONT_1:57

    for a,b be Real st a > 0 holds (( AffineMap (a,b)) .: [. 0 , 1.]) = [.b, (a + b).]

    proof

      let a,b be Real such that

       A1: a > 0 ;

      thus (( AffineMap (a,b)) .: [. 0 , 1.]) c= [.b, (a + b).]

      proof

        

         A2: (( AffineMap (a,b)) . 1) = (a + b) by Th49;

        let u be object;

        assume u in (( AffineMap (a,b)) .: [. 0 , 1.]);

        then

        consider r be Element of REAL such that

         A3: r in [. 0 , 1.] and

         A4: u = (( AffineMap (a,b)) . r) by FUNCT_2: 65;

        reconsider s = u as Real by A4;

        r <= 1 by A3, XXREAL_1: 1;

        then

         A5: s <= (a + b) by A1, A4, A2, Th53;

        

         A6: (( AffineMap (a,b)) . 0 ) = b by Th48;

         0 <= r by A3, XXREAL_1: 1;

        then b <= s by A1, A4, A6, Th53;

        hence thesis by A5, XXREAL_1: 1;

      end;

      let u be object;

      assume

       A7: u in [.b, (a + b).];

      then

      reconsider r = u as Element of REAL ;

      set s = ((r - b) / a);

      

       A8: (( AffineMap (a,b)) . s) = ((a * s) + b) by Def4

      .= ((r - b) + b) by A1, XCMPLX_1: 87

      .= r;

      r <= (a + b) by A7, XXREAL_1: 1;

      then (r - b) <= a by XREAL_1: 20;

      then s <= (a / a) by A1, XREAL_1: 72;

      then

       A9: s <= 1 by A1, XCMPLX_1: 60;

      b <= r by A7, XXREAL_1: 1;

      then 0 <= (r - b) by XREAL_1: 48;

      then s in [. 0 , 1.] by A1, A9, XXREAL_1: 1;

      hence thesis by A8, FUNCT_2: 35;

    end;