fcont_2.miz



    begin

    reserve n,m for Element of NAT ;

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

    reserve s,g,r,t,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;

      :: FCONT_2:def1

      attr f is uniformly_continuous means for r st 0 < r holds ex s st 0 < s & for x1, x2 st x1 in ( dom f) & x2 in ( dom f) & |.(x1 - x2).| < s holds |.((f . x1) - (f . x2)).| < r;

    end

    theorem :: FCONT_2:1

    

     Th1: (f | X) is uniformly_continuous iff for r st 0 < r holds ex s st 0 < s & for x1, x2 st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds |.((f . x1) - (f . x2)).| < r

    proof

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

      proof

        assume

         A1: (f | X) is uniformly_continuous;

        let r;

        assume 0 < r;

        then

        consider s such that

         A2: 0 < s and

         A3: for x1, x2 st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds |.(((f | X) . x1) - ((f | X) . x2)).| < r by A1;

        take s;

        thus 0 < s by A2;

        let x1, x2;

        assume that

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

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

        

         A6: ((f | X) . x2) = (f . x2) by A5, FUNCT_1: 47;

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

        hence thesis by A3, A4, A5, A6;

      end;

      assume

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

      let r;

      assume 0 < r;

      then

      consider s such that

       A8: 0 < s and

       A9: for x1, x2 st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds |.((f . x1) - (f . x2)).| < r by A7;

      take s;

      thus 0 < s by A8;

      let x1, x2;

      assume that

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

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

      

       A12: ((f | X) . x2) = (f . x2) by A11, FUNCT_1: 47;

      ((f | X) . x1) = (f . x1) by A10, FUNCT_1: 47;

      hence thesis by A9, A10, A11, A12;

    end;

    theorem :: FCONT_2:2

    

     Th2: (f | X) is uniformly_continuous & X1 c= X implies (f | X1) is uniformly_continuous

    proof

      assume that

       A1: (f | X) is uniformly_continuous and

       A2: X1 c= X;

      now

        let r;

        assume 0 < r;

        then

        consider s such that

         A3: 0 < s and

         A4: for x1, x2 st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds |.((f . x1) - (f . x2)).| < r by A1, Th1;

        take s;

        thus 0 < s by A3;

        let x1, x2;

        assume that

         A5: x1 in ( dom (f | X1)) and

         A6: x2 in ( dom (f | X1)) and

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

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

        then ( dom (f | X1)) c= ( dom (f | X)) by RELAT_1: 11;

        hence |.((f . x1) - (f . x2)).| < r by A4, A5, A6, A7;

      end;

      hence thesis by Th1;

    end;

    theorem :: FCONT_2:3

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

    proof

      assume that

       A1: X c= ( dom f1) and

       A2: X1 c= ( dom f2);

      

       A3: (X /\ X1) c= ( dom f2) by A2, XBOOLE_1: 108;

      (X /\ X1) c= ( dom f1) by A1, XBOOLE_1: 108;

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

      then

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

      assume that

       A5: (f1 | X) is uniformly_continuous and

       A6: (f2 | X1) is uniformly_continuous;

      

       A7: (f2 | (X /\ X1)) is uniformly_continuous by A6, Th2, XBOOLE_1: 17;

      

       A8: (f1 | (X /\ X1)) is uniformly_continuous by A5, Th2, XBOOLE_1: 17;

      now

        let r;

        

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

        assume 0 < r;

        then

         A10: 0 < (r / 2) by XREAL_1: 215;

        then

        consider s such that

         A11: 0 < s and

         A12: for x1, x2 st x1 in ( dom (f1 | (X /\ X1))) & x2 in ( dom (f1 | (X /\ X1))) & |.(x1 - x2).| < s holds |.((f1 . x1) - (f1 . x2)).| < (r / 2) by A8, Th1;

        consider g such that

         A13: 0 < g and

         A14: for x1, x2 st x1 in ( dom (f2 | (X /\ X1))) & x2 in ( dom (f2 | (X /\ X1))) & |.(x1 - x2).| < g holds |.((f2 . x1) - (f2 . x2)).| < (r / 2) by A7, A10, Th1;

        take p = ( min (s,g));

        thus 0 < p by A11, A13, XXREAL_0: 15;

        let x1, x2;

        assume that

         A15: x1 in ( dom ((f1 + f2) | (X /\ X1))) and

         A16: x2 in ( dom ((f1 + f2) | (X /\ X1))) and

         A17: |.(x1 - x2).| < p;

        

         A18: x2 in (X /\ X1) by A16, RELAT_1: 57;

        

         A19: x2 in ( dom (f1 + f2)) by A16, RELAT_1: 57;

        then x2 in ( dom f2) by A9, XBOOLE_0:def 4;

        then

         A20: x2 in ( dom (f2 | (X /\ X1))) by A18, RELAT_1: 57;

        p <= g by XXREAL_0: 17;

        then

         A21: |.(x1 - x2).| < g by A17, XXREAL_0: 2;

        

         A22: x1 in (X /\ X1) by A15, RELAT_1: 57;

        x2 in ( dom f1) by A9, A19, XBOOLE_0:def 4;

        then

         A23: x2 in ( dom (f1 | (X /\ X1))) by A18, RELAT_1: 57;

        p <= s by XXREAL_0: 17;

        then

         A24: |.(x1 - x2).| < s by A17, XXREAL_0: 2;

        

         A25: x1 in ( dom (f1 + f2)) by A15, RELAT_1: 57;

        then x1 in ( dom f2) by A9, XBOOLE_0:def 4;

        then x1 in ( dom (f2 | (X /\ X1))) by A22, RELAT_1: 57;

        then

         A26: |.((f2 . x1) - (f2 . x2)).| < (r / 2) by A14, A21, A20;

        x1 in ( dom f1) by A9, A25, XBOOLE_0:def 4;

        then x1 in ( dom (f1 | (X /\ X1))) by A22, RELAT_1: 57;

        then |.((f1 . x1) - (f1 . x2)).| < (r / 2) by A12, A24, A23;

        then

         A27: ( |.((f1 . x1) - (f1 . x2)).| + |.((f2 . x1) - (f2 . x2)).|) < ((r / 2) + (r / 2)) by A26, XREAL_1: 8;

        

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

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

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

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

        hence |.(((f1 + f2) . x1) - ((f1 + f2) . x2)).| < r by A27, A28, XXREAL_0: 2;

      end;

      hence thesis by Th1;

    end;

    theorem :: FCONT_2:4

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

    proof

      assume that

       A1: X c= ( dom f1) and

       A2: X1 c= ( dom f2);

      

       A3: (X /\ X1) c= ( dom f2) by A2, XBOOLE_1: 108;

      (X /\ X1) c= ( dom f1) by A1, XBOOLE_1: 108;

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

      then

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

      assume that

       A5: (f1 | X) is uniformly_continuous and

       A6: (f2 | X1) is uniformly_continuous;

      

       A7: (f2 | (X /\ X1)) is uniformly_continuous by A6, Th2, XBOOLE_1: 17;

      

       A8: (f1 | (X /\ X1)) is uniformly_continuous by A5, Th2, XBOOLE_1: 17;

      now

        let r;

        

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

        assume 0 < r;

        then

         A10: 0 < (r / 2) by XREAL_1: 215;

        then

        consider s such that

         A11: 0 < s and

         A12: for x1, x2 st x1 in ( dom (f1 | (X /\ X1))) & x2 in ( dom (f1 | (X /\ X1))) & |.(x1 - x2).| < s holds |.((f1 . x1) - (f1 . x2)).| < (r / 2) by A8, Th1;

        consider g such that

         A13: 0 < g and

         A14: for x1, x2 st x1 in ( dom (f2 | (X /\ X1))) & x2 in ( dom (f2 | (X /\ X1))) & |.(x1 - x2).| < g holds |.((f2 . x1) - (f2 . x2)).| < (r / 2) by A7, A10, Th1;

        take p = ( min (s,g));

        thus 0 < p by A11, A13, XXREAL_0: 15;

        let x1, x2;

        assume that

         A15: x1 in ( dom ((f1 - f2) | (X /\ X1))) and

         A16: x2 in ( dom ((f1 - f2) | (X /\ X1))) and

         A17: |.(x1 - x2).| < p;

        

         A18: x2 in (X /\ X1) by A16, RELAT_1: 57;

        

         A19: x2 in ( dom (f1 - f2)) by A16, RELAT_1: 57;

        then x2 in ( dom f2) by A9, XBOOLE_0:def 4;

        then

         A20: x2 in ( dom (f2 | (X /\ X1))) by A18, RELAT_1: 57;

        p <= g by XXREAL_0: 17;

        then

         A21: |.(x1 - x2).| < g by A17, XXREAL_0: 2;

        

         A22: x1 in (X /\ X1) by A15, RELAT_1: 57;

        x2 in ( dom f1) by A9, A19, XBOOLE_0:def 4;

        then

         A23: x2 in ( dom (f1 | (X /\ X1))) by A18, RELAT_1: 57;

        p <= s by XXREAL_0: 17;

        then

         A24: |.(x1 - x2).| < s by A17, XXREAL_0: 2;

        

         A25: x1 in ( dom (f1 - f2)) by A15, RELAT_1: 57;

        then x1 in ( dom f2) by A9, XBOOLE_0:def 4;

        then x1 in ( dom (f2 | (X /\ X1))) by A22, RELAT_1: 57;

        then

         A26: |.((f2 . x1) - (f2 . x2)).| < (r / 2) by A14, A21, A20;

        x1 in ( dom f1) by A9, A25, XBOOLE_0:def 4;

        then x1 in ( dom (f1 | (X /\ X1))) by A22, RELAT_1: 57;

        then |.((f1 . x1) - (f1 . x2)).| < (r / 2) by A12, A24, A23;

        then

         A27: ( |.((f1 . x1) - (f1 . x2)).| + |.((f2 . x1) - (f2 . x2)).|) < ((r / 2) + (r / 2)) by A26, XREAL_1: 8;

        

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

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

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

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

        hence |.(((f1 - f2) . x1) - ((f1 - f2) . x2)).| < r by A27, A28, XXREAL_0: 2;

      end;

      hence thesis by Th1;

    end;

    theorem :: FCONT_2:5

    

     Th5: X c= ( dom f) & (f | X) is uniformly_continuous implies ((p (#) f) | X) is uniformly_continuous

    proof

      assume X c= ( dom f);

      then

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

      assume

       A2: (f | X) is uniformly_continuous;

      per cases ;

        suppose

         A3: p = 0 ;

        now

          let r;

          assume

           A4: 0 < r;

          then

          consider s such that

           A5: 0 < s and for x1, x2 st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds |.((f . x1) - (f . x2)).| < r by A2, Th1;

          take s;

          thus 0 < s by A5;

          let x1, x2;

          assume that

           A6: x1 in ( dom ((p (#) f) | X)) and

           A7: x2 in ( dom ((p (#) f) | X)) and |.(x1 - x2).| < s;

          

           A8: x2 in X by A7, RELAT_1: 57;

          x1 in X by A6, RELAT_1: 57;

          

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

          .= |.( 0 - (p * (f . x2))).| by A1, A3, A8, VALUED_1:def 5

          .= 0 by A3, ABSVALUE: 2;

          hence |.(((p (#) f) . x1) - ((p (#) f) . x2)).| < r by A4;

        end;

        hence thesis by Th1;

      end;

        suppose

         A9: p <> 0 ;

        then

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

        

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

        now

          let r;

          assume 0 < r;

          then 0 < (r / |.p.|) by A10, XREAL_1: 139;

          then

          consider s such that

           A12: 0 < s and

           A13: for x1, x2 st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds |.((f . x1) - (f . x2)).| < (r / |.p.|) by A2, Th1;

          take s;

          thus 0 < s by A12;

          let x1, x2;

          assume that

           A14: x1 in ( dom ((p (#) f) | X)) and

           A15: x2 in ( dom ((p (#) f) | X)) and

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

          

           A17: x2 in X by A15, RELAT_1: 57;

          

           A18: x1 in X by A14, RELAT_1: 57;

          

          then

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

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

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

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

          x2 in ( dom (p (#) f)) by A15, RELAT_1: 57;

          then x2 in ( dom f) by VALUED_1:def 5;

          then

           A20: x2 in ( dom (f | X)) by A17, RELAT_1: 57;

          x1 in ( dom (p (#) f)) by A14, RELAT_1: 57;

          then x1 in ( dom f) by VALUED_1:def 5;

          then x1 in ( dom (f | X)) by A18, RELAT_1: 57;

          then ( |.p.| * |.((f . x1) - (f . x2)).|) < ((r / |.p.|) * |.p.|) by A10, A13, A16, A20, XREAL_1: 68;

          hence |.(((p (#) f) . x1) - ((p (#) f) . x2)).| < r by A11, A19, XCMPLX_1: 87;

        end;

        hence thesis by Th1;

      end;

    end;

    theorem :: FCONT_2:6

    X c= ( dom f) & (f | X) is uniformly_continuous implies (( - f) | X) is uniformly_continuous by Th5;

    theorem :: FCONT_2:7

    (f | X) is uniformly_continuous implies (( abs f) | X) is uniformly_continuous

    proof

      assume

       A1: (f | X) is uniformly_continuous;

      now

        let r;

        assume 0 < r;

        then

        consider s such that

         A2: 0 < s and

         A3: for x1, x2 st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds |.((f . x1) - (f . x2)).| < r by A1, Th1;

        take s;

        thus 0 < s by A2;

        let x1, x2;

        assume that

         A4: x1 in ( dom (( abs f) | X)) and

         A5: x2 in ( dom (( abs f) | X)) and

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

        x2 in ( dom ( abs f)) by A5, RELAT_1: 57;

        then

         A7: x2 in ( dom f) by VALUED_1:def 11;

        x2 in X by A5, RELAT_1: 57;

        then

         A8: x2 in ( dom (f | X)) by A7, RELAT_1: 57;

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

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

        then

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

        x1 in ( dom ( abs f)) by A4, RELAT_1: 57;

        then

         A10: x1 in ( dom f) by VALUED_1:def 11;

        x1 in X by A4, RELAT_1: 57;

        then x1 in ( dom (f | X)) by A10, RELAT_1: 57;

        then |.((f . x1) - (f . x2)).| < r by A3, A6, A8;

        hence |.((( abs f) . x1) - (( abs f) . x2)).| < r by A9, XXREAL_0: 2;

      end;

      hence thesis by Th1;

    end;

    theorem :: FCONT_2:8

    X c= ( dom f1) & X1 c= ( dom f2) & (f1 | X) is uniformly_continuous & (f2 | X1) is uniformly_continuous & (f1 | Z) is bounded & (f2 | Z1) is bounded implies ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) is uniformly_continuous

    proof

      assume that

       A1: X c= ( dom f1) and

       A2: X1 c= ( dom f2);

      assume that

       A3: (f1 | X) is uniformly_continuous and

       A4: (f2 | X1) is uniformly_continuous and

       A5: (f1 | Z) is bounded and

       A6: (f2 | Z1) is bounded;

      consider x1 be Real such that

       A7: for r be object st r in (Z /\ ( dom f1)) holds |.(f1 . r).| <= x1 by A5, RFUNCT_1: 73;

      consider x2 be Real such that

       A8: for r be object st r in (Z1 /\ ( dom f2)) holds |.(f2 . r).| <= x2 by A6, RFUNCT_1: 73;

      reconsider x1, x2 as Real;

      set M1 = ( |.x1.| + 1);

      set M2 = ( |.x2.| + 1);

      set M = ( max (M1,M2));

       A9:

      now

        let r;

        

         A10: M1 <= M by XXREAL_0: 25;

        assume r in (((X /\ Z) /\ X1) /\ Z1);

        then

         A11: r in ((X /\ Z) /\ (X1 /\ Z1)) by XBOOLE_1: 16;

        then

         A12: r in (X /\ Z) by XBOOLE_0:def 4;

        then

         A13: r in Z by XBOOLE_0:def 4;

        r in X by A12, XBOOLE_0:def 4;

        then r in (Z /\ ( dom f1)) by A1, A13, XBOOLE_0:def 4;

        then

         A14: |.(f1 . r).| <= x1 by A7;

        (x1 + 0 ) < M1 by ABSVALUE: 4, XREAL_1: 8;

        then |.(f1 . r).| < M1 by A14, XXREAL_0: 2;

        hence |.(f1 . r).| < M by A10, XXREAL_0: 2;

        

         A15: M2 <= M by XXREAL_0: 25;

        

         A16: r in (X1 /\ Z1) by A11, XBOOLE_0:def 4;

        then

         A17: r in Z1 by XBOOLE_0:def 4;

        r in X1 by A16, XBOOLE_0:def 4;

        then r in (Z1 /\ ( dom f2)) by A2, A17, XBOOLE_0:def 4;

        then

         A18: |.(f2 . r).| <= x2 by A8;

        (x2 + 0 ) < M2 by ABSVALUE: 4, XREAL_1: 8;

        then |.(f2 . r).| < M2 by A18, XXREAL_0: 2;

        hence |.(f2 . r).| < M by A15, XXREAL_0: 2;

      end;

      

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

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

      then

       A20: 0 < M by A19, XXREAL_0: 16;

      then

       A21: 0 < (2 * M) by XREAL_1: 129;

      for r st 0 < r holds ex s st 0 < s & for x1, x2 st x1 in ( dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1))) & x2 in ( dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1))) & |.(x1 - x2).| < s holds |.(((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)).| < r

      proof

        let r;

        assume 0 < r;

        then

         A22: 0 < (r / (2 * M)) by A21, XREAL_1: 139;

        then

        consider s such that

         A23: 0 < s and

         A24: for x1, x2 st x1 in ( dom (f1 | X)) & x2 in ( dom (f1 | X)) & |.(x1 - x2).| < s holds |.((f1 . x1) - (f1 . x2)).| < (r / (2 * M)) by A3, Th1;

        consider g such that

         A25: 0 < g and

         A26: for x1, x2 st x1 in ( dom (f2 | X1)) & x2 in ( dom (f2 | X1)) & |.(x1 - x2).| < g holds |.((f2 . x1) - (f2 . x2)).| < (r / (2 * M)) by A4, A22, Th1;

        take p = ( min (s,g));

        thus 0 < p by A23, A25, XXREAL_0: 15;

        let y1,y2 be Real;

        assume that

         A27: y1 in ( dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1))) and

         A28: y2 in ( dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)));

        assume

         A29: |.(y1 - y2).| < p;

        

         A30: y2 in (((X /\ Z) /\ X1) /\ Z1) by A28, RELAT_1: 57;

        then

         A31: y2 in ((X /\ Z) /\ (X1 /\ Z1)) by XBOOLE_1: 16;

        then y2 in (X /\ Z) by XBOOLE_0:def 4;

        then y2 in X by XBOOLE_0:def 4;

        then

         A32: y2 in ( dom (f1 | X)) by A1, RELAT_1: 62;

        

         A33: y1 in (((X /\ Z) /\ X1) /\ Z1) by A27, RELAT_1: 57;

        then

         A34: y1 in ((X /\ Z) /\ (X1 /\ Z1)) by XBOOLE_1: 16;

        then y1 in (X /\ Z) by XBOOLE_0:def 4;

        then y1 in X by XBOOLE_0:def 4;

        then

         A35: y1 in ( dom (f1 | X)) by A1, RELAT_1: 62;

        y2 in (X1 /\ Z1) by A31, XBOOLE_0:def 4;

        then y2 in X1 by XBOOLE_0:def 4;

        then

         A36: y2 in ( dom (f2 | X1)) by A2, RELAT_1: 62;

        y1 in (X1 /\ Z1) by A34, XBOOLE_0:def 4;

        then y1 in X1 by XBOOLE_0:def 4;

        then

         A37: y1 in ( dom (f2 | X1)) by A2, RELAT_1: 62;

        p <= g by XXREAL_0: 17;

        then |.(y1 - y2).| < g by A29, XXREAL_0: 2;

        then

         A38: |.((f2 . y1) - (f2 . y2)).| < (r / (2 * M)) by A26, A37, A36;

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

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

        

         A40: |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| = ( |.(f1 . y1).| * |.((f2 . y1) - (f2 . y2)).|) by COMPLEX1: 65;

        

         A41: |.(f2 . y2).| < M by A9, A30;

        

         A42: 0 <= |.(f2 . y2).| by COMPLEX1: 46;

        

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

        

         A44: |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| = ( |.(f2 . y2).| * |.((f1 . y1) - (f1 . y2)).|) by COMPLEX1: 65;

        p <= s by XXREAL_0: 17;

        then |.(y1 - y2).| < s by A29, XXREAL_0: 2;

        then |.((f1 . y1) - (f1 . y2)).| < (r / (2 * M)) by A24, A35, A32;

        then

         A45: |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).| < (M * (r / (2 * M))) by A44, A41, A43, A42, XREAL_1: 96;

        

         A46: 0 <= |.(f1 . y1).| by COMPLEX1: 46;

        

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

         |.(f1 . y1).| < M by A9, A33;

        then |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| < (M * (r / (2 * M))) by A40, A38, A47, A46, XREAL_1: 96;

        then

         A48: ( |.((f1 . y1) * ((f2 . y1) - (f2 . y2))).| + |.(((f1 . y1) - (f1 . y2)) * (f2 . y2)).|) < ((M * (r / (2 * M))) + (M * (r / (2 * M)))) by A45, XREAL_1: 8;

        ((M * (r / (2 * M))) + (M * (r / (2 * M)))) = (M * ((r / (M * 2)) + (r / (M * 2))))

        .= ((r / M) * M) by XCMPLX_1: 118

        .= r by A20, XCMPLX_1: 87;

        hence thesis by A39, A48, XXREAL_0: 2;

      end;

      hence thesis by Th1;

    end;

    theorem :: FCONT_2:9

    

     Th9: X c= ( dom f) & (f | X) is uniformly_continuous implies (f | X) is continuous

    proof

      assume

       A1: X c= ( dom f);

      assume

       A2: (f | X) is uniformly_continuous;

      now

        let x0,r be Real;

        assume that

         A3: x0 in X and

         A4: 0 < r;

        

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

        consider s such that

         A6: 0 < s and

         A7: for x1, x2 st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) & |.(x1 - x2).| < s holds |.((f . x1) - (f . x2)).| < r by A2, A4, Th1;

        reconsider s as Real;

        take s;

        thus 0 < s by A6;

        let x1 be Real;

        assume that

         A8: x1 in X and

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

        x1 in ( dom (f | X)) by A1, A8, RELAT_1: 62;

        hence |.((f . x1) - (f . x0)).| < r by A7, A9, A5;

      end;

      hence thesis by A1, FCONT_1: 14;

    end;

    theorem :: FCONT_2:10

    

     Th10: (f | X) is Lipschitzian implies (f | X) is uniformly_continuous

    proof

      assume (f | X) is Lipschitzian;

      then

      consider r be Real such that

       A1: 0 < r and

       A2: for x1,x2 be Real st x1 in ( dom (f | X)) & x2 in ( dom (f | X)) holds |.((f . x1) - (f . x2)).| <= (r * |.(x1 - x2).|) by FCONT_1: 32;

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

      proof

        let p such that

         A3: 0 < p;

        take s = (p / r);

        thus 0 < s by A1, A3, XREAL_1: 139;

        let x1, x2;

        assume that

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

         A5: x2 in ( dom (f | X)) and

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

        

         A7: (r * |.(x1 - x2).|) < (s * r) by A1, A6, XREAL_1: 68;

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

        then |.((f . x1) - (f . x2)).| < ((p / r) * r) by A7, XXREAL_0: 2;

        hence |.((f . x1) - (f . x2)).| < p by A1, XCMPLX_1: 87;

      end;

      hence thesis by Th1;

    end;

    theorem :: FCONT_2:11

    

     Th11: for f, Y st Y c= ( dom f) & Y is compact & (f | Y) is continuous holds (f | Y) is uniformly_continuous

    proof

      let f, Y such that

       A1: Y c= ( dom f) and

       A2: Y is compact and

       A3: (f | Y) is continuous;

      assume not thesis;

      then

      consider r such that

       A4: 0 < r and

       A5: for s st 0 < s holds ex x1, x2 st x1 in ( dom (f | Y)) & x2 in ( dom (f | Y)) & |.(x1 - x2).| < s & not |.((f . x1) - (f . x2)).| < r by Th1;

      defpred P[ Element of NAT , Real] means $2 in Y & ex x2 be Element of REAL st x2 in Y & |.($2 - x2).| < (1 / ($1 + 1)) & not |.((f . $2) - (f . x2)).| < r;

       A6:

      now

        let n;

        consider x1 such that

         A7: ex x2 st x1 in ( dom (f | Y)) & x2 in ( dom (f | Y)) & |.(x1 - x2).| < (1 / (n + 1)) & not |.((f . x1) - (f . x2)).| < r by A5, XREAL_1: 139;

        reconsider x1 as Element of REAL by XREAL_0:def 1;

        take x1;

        ( dom (f | Y)) = Y by A1, RELAT_1: 62;

        hence P[n, x1] by A7;

      end;

      consider s1 such that

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

      now

        let x be object;

        assume x in ( rng s1);

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

        hence x in Y by A8;

      end;

      then

       A9: ( rng s1) c= Y by TARSKI:def 3;

      then

      consider q1 such that

       A10: q1 is subsequence of s1 and

       A11: q1 is convergent and

       A12: ( lim q1) in Y by A2, RCOMP_1:def 3;

      ( lim q1) in ( dom (f | Y)) by A1, A12, RELAT_1: 57;

      then

       A13: (f | Y) is_continuous_in ( lim q1) by A3, FCONT_1:def 2;

      ( rng q1) c= ( rng s1) by A10, VALUED_0: 21;

      then

       A14: ( rng q1) c= Y by A9, XBOOLE_1: 1;

      then ( rng q1) c= ( dom f) by A1, XBOOLE_1: 1;

      then ( rng q1) c= (( dom f) /\ Y) by A14, XBOOLE_1: 19;

      then

       A15: ( rng q1) c= ( dom (f | Y)) by RELAT_1: 61;

      then

       A16: ((f | Y) . ( lim q1)) = ( lim ((f | Y) /* q1)) by A11, A13, FCONT_1:def 1;

      

       A17: ((f | Y) /* q1) is convergent by A11, A13, A15, FCONT_1:def 1;

      defpred P[ Element of NAT , Real] means $2 in Y & |.((s1 . $1) - $2).| < (1 / ($1 + 1)) & not |.((f . (s1 . $1)) - (f . $2)).| < r;

      

       A18: for n holds ex x2 be Element of REAL st P[n, x2] by A8;

      consider s2 such that

       A19: for n holds P[n, (s2 . n)] from FUNCT_2:sch 3( A18);

      now

        let x be object;

        assume x in ( rng s2);

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

        hence x in Y by A19;

      end;

      then

       A20: ( rng s2) c= Y by TARSKI:def 3;

      consider Ns1 be increasing sequence of NAT such that

       A21: q1 = (s1 * Ns1) by A10, VALUED_0:def 17;

      set q2 = (q1 - ((s1 - s2) * Ns1));

       A22:

      now

        let n;

        

        thus (q2 . n) = (((s1 * Ns1) . n) - (((s1 - s2) * Ns1) . n)) by A21, RFUNCT_2: 1

        .= ((s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n)) by FUNCT_2: 15

        .= ((s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n))) by FUNCT_2: 15

        .= ((s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n)))) by RFUNCT_2: 1

        .= ((s2 * Ns1) . n) by FUNCT_2: 15;

      end;

      then

       A23: q2 = (s2 * Ns1) by FUNCT_2: 63;

      q2 is subsequence of s2 by A22, FUNCT_2: 63, VALUED_0:def 17;

      then ( rng q2) c= ( rng s2) by VALUED_0: 21;

      then

       A24: ( rng q2) c= Y by A20, XBOOLE_1: 1;

      then ( rng q2) c= ( dom f) by A1, XBOOLE_1: 1;

      then ( rng q2) c= (( dom f) /\ Y) by A24, XBOOLE_1: 19;

      then

       A25: ( rng q2) c= ( dom (f | Y)) by RELAT_1: 61;

       A26:

      now

        let p be Real such that

         A27: 0 < p;

        consider k be Nat such that

         A28: (p " ) < k by SEQ_4: 3;

        take k;

        let m be Nat;

        

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

         A30: |.((s1 . m) - (s2 . m)).| < (1 / (k + 1)) by A19, XXREAL_0: 2, A29;

        k < (k + 1) by NAT_1: 13;

        then (p " ) < (k + 1) by A28, XXREAL_0: 2;

        then (1 / (k + 1)) < (1 / (p " )) by A27, XREAL_1: 76;

        then

         A31: (1 / (k + 1)) < p by XCMPLX_1: 216;

         |.(((s1 - s2) . m) - 0 ).| = |.((s1 . m) - (s2 . m)).| by RFUNCT_2: 1;

        hence |.(((s1 - s2) . m) - 0 ).| < p by A31, A30, XXREAL_0: 2;

      end;

      then

       A32: (s1 - s2) is convergent by SEQ_2:def 6;

      

       A33: ((s1 - s2) * Ns1) is subsequence of (s1 - s2) by VALUED_0:def 17;

      then

       A34: ((s1 - s2) * Ns1) is convergent by A32, SEQ_4: 16;

      ( lim (s1 - s2)) = 0 by A26, A32, SEQ_2:def 7;

      then ( lim ((s1 - s2) * Ns1)) = 0 by A32, A33, SEQ_4: 17;

      

      then

       A35: ( lim q2) = (( lim q1) - 0 ) by A11, A34, SEQ_2: 12

      .= ( lim q1);

      

       A36: q2 is convergent by A11, A34, SEQ_2: 11;

      then

       A37: ((f | Y) /* q2) is convergent by A13, A35, A25, FCONT_1:def 1;

      then

       A38: (((f | Y) /* q1) - ((f | Y) /* q2)) is convergent by A17, SEQ_2: 11;

      ((f | Y) . ( lim q1)) = ( lim ((f | Y) /* q2)) by A13, A36, A35, A25, FCONT_1:def 1;

      

      then

       A39: ( lim (((f | Y) /* q1) - ((f | Y) /* q2))) = (((f | Y) . ( lim q1)) - ((f | Y) . ( lim q1))) by A17, A16, A37, SEQ_2: 12

      .= 0 ;

      now

        let n;

        consider k be Nat such that

         A40: for m be Nat st k <= m holds |.(((((f | Y) /* q1) - ((f | Y) /* q2)) . m) - 0 ).| < r by A4, A38, A39, SEQ_2:def 7;

        

         A41: (q1 . k) in ( rng q1) by VALUED_0: 28;

        

         A42: (q2 . k) in ( rng q2) by VALUED_0: 28;

        

         A43: k in NAT by ORDINAL1:def 12;

         |.(((((f | Y) /* q1) - ((f | Y) /* q2)) . k) - 0 ).| = |.((((f | Y) /* q1) . k) - (((f | Y) /* q2) . k)).| by RFUNCT_2: 1

        .= |.(((f | Y) . (q1 . k)) - (((f | Y) /* q2) . k)).| by A15, FUNCT_2: 108, A43

        .= |.(((f | Y) . (q1 . k)) - ((f | Y) . (q2 . k))).| by A25, FUNCT_2: 108, A43

        .= |.((f . (q1 . k)) - ((f | Y) . (q2 . k))).| by A15, A41, FUNCT_1: 47

        .= |.((f . (q1 . k)) - (f . (q2 . k))).| by A25, A42, FUNCT_1: 47

        .= |.((f . (s1 . (Ns1 . k))) - (f . ((s2 * Ns1) . k))).| by A21, A23, FUNCT_2: 15, A43

        .= |.((f . (s1 . (Ns1 . k))) - (f . (s2 . (Ns1 . k)))).| by FUNCT_2: 15, A43;

        hence contradiction by A19, A40;

      end;

      hence contradiction;

    end;

    theorem :: FCONT_2:12

    Y c= ( dom f) & Y is compact & (f | Y) is uniformly_continuous implies (f .: Y) is compact by Th9, FCONT_1: 29;

    theorem :: FCONT_2:13

    for f, Y st Y <> {} & Y c= ( dom f) & Y is compact & (f | Y) is uniformly_continuous holds ex x1, x2 st x1 in Y & x2 in Y & (f . x1) = ( upper_bound (f .: Y)) & (f . x2) = ( lower_bound (f .: Y)) by Th9, FCONT_1: 31;

    theorem :: FCONT_2:14

    X c= ( dom f) & (f | X) is constant implies (f | X) is uniformly_continuous by Th10;

    theorem :: FCONT_2:15

    

     Th15: p <= g & [.p, g.] c= ( dom f) & (f | [.p, g.]) is continuous implies for r st r in ( [.(f . p), (f . g).] \/ [.(f . g), (f . p).]) holds ex s st s in [.p, g.] & r = (f . s)

    proof

      assume that

       A1: p <= g and

       A2: [.p, g.] c= ( dom f) and

       A3: (f | [.p, g.]) is continuous;

      let r such that

       A4: r in ( [.(f . p), (f . g).] \/ [.(f . g), (f . p).]);

      

       A5: [.p, g.] is compact by RCOMP_1: 6;

      

       A6: (f . p) < (f . g) implies ex s st s in [.p, g.] & r = (f . s)

      proof

        r in REAL by XREAL_0:def 1;

        then

        reconsider f1 = ( [.p, g.] --> r) as Function of [.p, g.], REAL by FUNCOP_1: 45;

        assume that

         A7: (f . p) < (f . g) and

         A8: for s st s in [.p, g.] holds r <> (f . s);

        ( [.(f . p), (f . g).] \/ [.(f . g), (f . p).]) = ( [.(f . p), (f . g).] \/ {} ) by A7, XXREAL_1: 29

        .= [.(f . p), (f . g).];

        then r in { s : (f . p) <= s & s <= (f . g) } by A4, RCOMP_1:def 1;

        then

         A9: ex s st s = r & (f . p) <= s & s <= (f . g);

        p in [.p, g.] by A1, XXREAL_1: 1;

        then

         A10: r <> (f . p) by A8;

        reconsider f1 as PartFunc of REAL , REAL by RELSET_1: 7;

        

         A11: ( dom f1) = [.p, g.] by FUNCOP_1: 13;

        then

         A12: [.p, g.] c= (( dom f1) /\ ( dom f)) by A2, XBOOLE_1: 19;

        then

         A13: [.p, g.] c= ( dom (f1 - f)) by VALUED_1: 12;

        

         A14: (( abs (f1 - f)) " { 0 }) = {}

        proof

          assume (( abs (f1 - f)) " { 0 }) <> {} ;

          then

          consider x2 be Element of REAL such that

           A15: x2 in (( abs (f1 - f)) " { 0 }) by SUBSET_1: 4;

          x2 in ( dom ( abs (f1 - f))) by A15, FUNCT_1:def 7;

          then

           A16: x2 in ( dom (f1 - f)) by VALUED_1:def 11;

          then x2 in (( dom f1) /\ ( dom f)) by VALUED_1: 12;

          then

           A17: x2 in [.p, g.] by A11, XBOOLE_0:def 4;

          (( abs (f1 - f)) . x2) in { 0 } by A15, FUNCT_1:def 7;

          then (( abs (f1 - f)) . x2) = 0 by TARSKI:def 1;

          then |.((f1 - f) . x2).| = 0 by VALUED_1: 18;

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

          then ((f1 . x2) - (f . x2)) = 0 by A16, VALUED_1: 13;

          then (r - (f . x2)) = 0 by A17, FUNCOP_1: 7;

          hence contradiction by A8, A17;

        end;

        

         A18: ( dom (( abs (f1 - f)) ^ )) = (( dom ( abs (f1 - f))) \ (( abs (f1 - f)) " { 0 })) by RFUNCT_1:def 2

        .= ( dom (f1 - f)) by A14, VALUED_1:def 11

        .= ( [.p, g.] /\ ( dom f)) by A11, VALUED_1: 12

        .= [.p, g.] by A2, XBOOLE_1: 28;

        reconsider r as Element of REAL by XREAL_0:def 1;

        for x0 be Element of REAL st x0 in ( [.p, g.] /\ ( dom f1)) holds (f1 . x0) = r by A11, FUNCOP_1: 7;

        then (f1 | [.p, g.]) is constant by PARTFUN2: 57;

        then ((f1 - f) | [.p, g.]) is continuous by A3, A12, FCONT_1: 18;

        then (( abs (f1 - f)) | [.p, g.]) is continuous by A13, FCONT_1: 21;

        then ((( abs (f1 - f)) ^ ) | [.p, g.]) is continuous by A14, FCONT_1: 22;

        then ((( abs (f1 - f)) ^ ) .: [.p, g.]) is real-bounded by A5, A18, FCONT_1: 29, RCOMP_1: 10;

        then

        consider M be Real such that

         A19: M is UpperBound of ((( abs (f1 - f)) ^ ) .: [.p, g.]) by XXREAL_2:def 10;

        

         A20: for x1 be Real st x1 in ((( abs (f1 - f)) ^ ) .: [.p, g.]) holds x1 <= M by A19, XXREAL_2:def 1;

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

        then 0 < (( |.M.| + 1) " );

        then

         A21: 0 < (1 / ( |.M.| + 1)) by XCMPLX_1: 215;

        (f | [.p, g.]) is uniformly_continuous by A2, A3, Th11, RCOMP_1: 6;

        then

        consider s such that

         A22: 0 < s and

         A23: for x1, x2 st x1 in ( dom (f | [.p, g.])) & x2 in ( dom (f | [.p, g.])) & |.(x1 - x2).| < s holds |.((f . x1) - (f . x2)).| < (1 / ( |.M.| + 1)) by A21, Th1;

         A24:

        now

          let x1;

          assume

           A25: x1 in [.p, g.];

          then ((( abs (f1 - f)) ^ ) . x1) in ((( abs (f1 - f)) ^ ) .: [.p, g.]) by A18, FUNCT_1:def 6;

          then ((( abs (f1 - f)) ^ ) . x1) <= M by A20;

          then ((( abs (f1 - f)) . x1) " ) <= M by A18, A25, RFUNCT_1:def 2;

          then

           A26: ( |.((f1 - f) . x1).| " ) <= M by VALUED_1: 18;

          x1 in (( dom f1) /\ ( dom f)) by A2, A11, A25, XBOOLE_0:def 4;

          then x1 in ( dom (f1 - f)) by VALUED_1: 12;

          then ( |.((f1 . x1) - (f . x1)).| " ) <= M by A26, VALUED_1: 13;

          then

           A27: ( |.(r - (f . x1)).| " ) <= M by A25, FUNCOP_1: 7;

          (r - (f . x1)) <> 0 by A8, A25;

          then

           A28: 0 < |.(r - (f . x1)).| by COMPLEX1: 47;

          (M + 0 ) < ( |.M.| + 1) by ABSVALUE: 4, XREAL_1: 8;

          then ( |.(r - (f . x1)).| " ) < ( |.M.| + 1) by A27, XXREAL_0: 2;

          then (1 / ( |.M.| + 1)) < (1 / ( |.(r - (f . x1)).| " )) by A28, XREAL_1: 76;

          hence (1 / ( |.M.| + 1)) < |.(r - (f . x1)).| by XCMPLX_1: 216;

        end;

        now

          per cases ;

            suppose p = g;

            hence contradiction by A7;

          end;

            suppose p <> g;

            then p < g by A1, XXREAL_0: 1;

            then

             A29: 0 < (g - p) by XREAL_1: 50;

            then

             A30: 0 < ((g - p) / s) by A22, XREAL_1: 139;

            consider k be Nat such that

             A31: ((g - p) / s) < k by SEQ_4: 3;

            (((g - p) / s) * s) < (s * k) by A22, A31, XREAL_1: 68;

            then (g - p) < (s * k) by A22, XCMPLX_1: 87;

            then ((g - p) / k) < ((s * k) / k) by A31, A30, XREAL_1: 74;

            then ((g - p) / k) < ((s * k) * (k " )) by XCMPLX_0:def 9;

            then ((g - p) / k) < (s * (k * (k " )));

            then

             A32: ((g - p) / k) < (s * 1) by A31, A30, XCMPLX_0:def 7;

            deffunc F( Nat) = (p + (((g - p) / k) * $1));

            consider s1 such that

             A33: for n be Nat holds (s1 . n) = F(n) from SEQ_1:sch 1;

            

             A34: 0 < ((g - p) / k) by A29, A31, A30, XREAL_1: 139;

             A35:

            now

              let n;

              

               A36: ( dom (f | [.p, g.])) = [.p, g.] by A2, RELAT_1: 62;

              assume

               A37: n < k;

              then (((g - p) / k) * n) < (((g - p) / k) * k) by A34, XREAL_1: 68;

              then (((g - p) / k) * n) < (g - p) by A31, A30, XCMPLX_1: 87;

              then (p + (((g - p) / k) * n)) < (p + (g - p)) by XREAL_1: 6;

              then

               A38: (s1 . n) < (p + (g - p)) by A33;

              (n + 1) <= k by A37, NAT_1: 13;

              then (((g - p) / k) * (n + 1)) <= (((g - p) / k) * k) by A29, XREAL_1: 64;

              then (((g - p) / k) * (n + 1)) <= (g - p) by A31, A30, XCMPLX_1: 87;

              then (p + (((g - p) / k) * (n + 1))) <= (p + (g - p)) by XREAL_1: 7;

              then

               A39: (s1 . (n + 1)) <= (p + (g - p)) by A33;

              (p + 0 ) <= (p + (((g - p) / k) * n)) by A29, XREAL_1: 7;

              then p <= (s1 . n) by A33;

              then (s1 . n) in { x2 : p <= x2 & x2 <= g } by A38;

              hence

               A40: (s1 . n) in [.p, g.] by RCOMP_1:def 1;

              (p + 0 ) <= (p + (((g - p) / k) * (n + 1))) by A29, XREAL_1: 7;

              then p <= (s1 . (n + 1)) by A33;

              then (s1 . (n + 1)) in { x2 : p <= x2 & x2 <= g } by A39;

              hence

               A41: (s1 . (n + 1)) in [.p, g.] by RCOMP_1:def 1;

               |.((s1 . (n + 1)) - (s1 . n)).| = |.((p + (((g - p) / k) * (n + 1))) - (s1 . n)).| by A33

              .= |.((p + (((g - p) / k) * (n + 1))) - (p + (((g - p) / k) * n))).| by A33

              .= ((g - p) / k) by A29, ABSVALUE:def 1;

              hence |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < (1 / ( |.M.| + 1)) by A23, A32, A40, A41, A36;

            end;

            defpred P[ Nat] means r <= (f . (s1 . $1));

            

             A42: (s1 . k) = (p + (((g - p) / k) * k)) by A33

            .= (p + (g - p)) by A31, A30, XCMPLX_1: 87

            .= g;

            then

             A43: ex n be Nat st P[n] by A9;

            consider l be Nat such that

             A44: P[l] & for m be Nat st P[m] holds l <= m from NAT_1:sch 5( A43);

            (s1 . 0 ) = (p + (((g - p) / k) * 0 )) by A33

            .= p;

            then l <> 0 by A9, A10, A44, XXREAL_0: 1;

            then

            consider l1 be Nat such that

             A45: l = (l1 + 1) by NAT_1: 6;

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

            

             A46: (r - (f . (s1 . l1))) <= ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) by A44, A45, XREAL_1: 9;

            (l1 + 1) <= k by A9, A42, A44, A45;

            then

             A47: l1 < k by NAT_1: 13;

            then

             A48: |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| < (1 / ( |.M.| + 1)) by A35;

            (f . (s1 . l1)) < r

            proof

              assume r <= (f . (s1 . l1));

              then l <= l1 by A44;

              then (l + 0 ) < l by A45, XREAL_1: 8;

              hence contradiction;

            end;

            then

             A49: 0 < (r - (f . (s1 . l1))) by XREAL_1: 50;

            then 0 < ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) by A44, A45, XREAL_1: 9;

            then |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| = ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) by ABSVALUE:def 1;

            then

             A50: |.(r - (f . (s1 . l1))).| <= |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| by A49, A46, ABSVALUE:def 1;

            (s1 . l1) in [.p, g.] by A35, A47;

            hence contradiction by A24, A50, A48, XXREAL_0: 2;

          end;

        end;

        hence contradiction;

      end;

      

       A51: (f . g) < (f . p) implies ex s st s in [.p, g.] & r = (f . s)

      proof

        r in REAL by XREAL_0:def 1;

        then

        reconsider f1 = ( [.p, g.] --> r) as Function of [.p, g.], REAL by FUNCOP_1: 45;

        assume that

         A52: (f . g) < (f . p) and

         A53: for s st s in [.p, g.] holds r <> (f . s);

        ( [.(f . p), (f . g).] \/ [.(f . g), (f . p).]) = ( {} \/ [.(f . g), (f . p).]) by A52, XXREAL_1: 29

        .= [.(f . g), (f . p).];

        then r in { s : (f . g) <= s & s <= (f . p) } by A4, RCOMP_1:def 1;

        then

         A54: ex s st s = r & (f . g) <= s & s <= (f . p);

        g in { s : p <= s & s <= g } by A1;

        then g in [.p, g.] by RCOMP_1:def 1;

        then

         A55: r <> (f . g) by A53;

        reconsider f1 as PartFunc of REAL , REAL by RELSET_1: 7;

        

         A56: ( dom f1) = [.p, g.] by FUNCOP_1: 13;

        then

         A57: [.p, g.] c= (( dom f1) /\ ( dom f)) by A2, XBOOLE_1: 19;

        then

         A58: [.p, g.] c= ( dom (f1 - f)) by VALUED_1: 12;

        

         A59: (( abs (f1 - f)) " { 0 }) = {}

        proof

          assume (( abs (f1 - f)) " { 0 }) <> {} ;

          then

          consider x2 be Element of REAL such that

           A60: x2 in (( abs (f1 - f)) " { 0 }) by SUBSET_1: 4;

          x2 in ( dom ( abs (f1 - f))) by A60, FUNCT_1:def 7;

          then

           A61: x2 in ( dom (f1 - f)) by VALUED_1:def 11;

          then x2 in (( dom f1) /\ ( dom f)) by VALUED_1: 12;

          then

           A62: x2 in [.p, g.] by A56, XBOOLE_0:def 4;

          (( abs (f1 - f)) . x2) in { 0 } by A60, FUNCT_1:def 7;

          then (( abs (f1 - f)) . x2) = 0 by TARSKI:def 1;

          then |.((f1 - f) . x2).| = 0 by VALUED_1: 18;

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

          then ((f1 . x2) - (f . x2)) = 0 by A61, VALUED_1: 13;

          then (r - (f . x2)) = 0 by A62, FUNCOP_1: 7;

          hence contradiction by A53, A62;

        end;

        

         A63: ( dom (( abs (f1 - f)) ^ )) = (( dom ( abs (f1 - f))) \ (( abs (f1 - f)) " { 0 })) by RFUNCT_1:def 2

        .= ( dom (f1 - f)) by A59, VALUED_1:def 11

        .= ( [.p, g.] /\ ( dom f)) by A56, VALUED_1: 12

        .= [.p, g.] by A2, XBOOLE_1: 28;

        reconsider r as Element of REAL by XREAL_0:def 1;

        for x0 be Element of REAL st x0 in ( [.p, g.] /\ ( dom f1)) holds (f1 . x0) = r by A56, FUNCOP_1: 7;

        then (f1 | [.p, g.]) is constant by PARTFUN2: 57;

        then ((f1 - f) | [.p, g.]) is continuous by A3, A57, FCONT_1: 18;

        then (( abs (f1 - f)) | [.p, g.]) is continuous by A58, FCONT_1: 21;

        then ((( abs (f1 - f)) ^ ) | [.p, g.]) is continuous by A59, FCONT_1: 22;

        then ((( abs (f1 - f)) ^ ) .: [.p, g.]) is real-bounded by A5, A63, FCONT_1: 29, RCOMP_1: 10;

        then

        consider M be Real such that

         A64: M is UpperBound of ((( abs (f1 - f)) ^ ) .: [.p, g.]) by XXREAL_2:def 10;

        

         A65: for x1 be Real st x1 in ((( abs (f1 - f)) ^ ) .: [.p, g.]) holds x1 <= M by A64, XXREAL_2:def 1;

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

        then 0 < (( |.M.| + 1) " );

        then

         A66: 0 < (1 / ( |.M.| + 1)) by XCMPLX_1: 215;

        (f | [.p, g.]) is uniformly_continuous by A2, A3, Th11, RCOMP_1: 6;

        then

        consider s such that

         A67: 0 < s and

         A68: for x1, x2 st x1 in ( dom (f | [.p, g.])) & x2 in ( dom (f | [.p, g.])) & |.(x1 - x2).| < s holds |.((f . x1) - (f . x2)).| < (1 / ( |.M.| + 1)) by A66, Th1;

         A69:

        now

          let x1;

          assume

           A70: x1 in [.p, g.];

          then ((( abs (f1 - f)) ^ ) . x1) in ((( abs (f1 - f)) ^ ) .: [.p, g.]) by A63, FUNCT_1:def 6;

          then ((( abs (f1 - f)) ^ ) . x1) <= M by A65;

          then ((( abs (f1 - f)) . x1) " ) <= M by A63, A70, RFUNCT_1:def 2;

          then

           A71: ( |.((f1 - f) . x1).| " ) <= M by VALUED_1: 18;

          x1 in (( dom f1) /\ ( dom f)) by A2, A56, A70, XBOOLE_0:def 4;

          then x1 in ( dom (f1 - f)) by VALUED_1: 12;

          then ( |.((f1 . x1) - (f . x1)).| " ) <= M by A71, VALUED_1: 13;

          then

           A72: ( |.(r - (f . x1)).| " ) <= M by A70, FUNCOP_1: 7;

          (r - (f . x1)) <> 0 by A53, A70;

          then

           A73: 0 < |.(r - (f . x1)).| by COMPLEX1: 47;

          (M + 0 ) < ( |.M.| + 1) by ABSVALUE: 4, XREAL_1: 8;

          then ( |.(r - (f . x1)).| " ) < ( |.M.| + 1) by A72, XXREAL_0: 2;

          then (1 / ( |.M.| + 1)) < (1 / ( |.(r - (f . x1)).| " )) by A73, XREAL_1: 76;

          hence (1 / ( |.M.| + 1)) < |.(r - (f . x1)).| by XCMPLX_1: 216;

        end;

        now

          per cases ;

            suppose p = g;

            hence contradiction by A52;

          end;

            suppose p <> g;

            then p < g by A1, XXREAL_0: 1;

            then

             A74: 0 < (g - p) by XREAL_1: 50;

            then

             A75: 0 < ((g - p) / s) by A67, XREAL_1: 139;

            consider k be Nat such that

             A76: ((g - p) / s) < k by SEQ_4: 3;

            (((g - p) / s) * s) < (s * k) by A67, A76, XREAL_1: 68;

            then (g - p) < (s * k) by A67, XCMPLX_1: 87;

            then ((g - p) / k) < ((s * k) / k) by A76, A75, XREAL_1: 74;

            then ((g - p) / k) < ((s * k) * (k " )) by XCMPLX_0:def 9;

            then ((g - p) / k) < (s * (k * (k " )));

            then

             A77: ((g - p) / k) < (s * 1) by A76, A75, XCMPLX_0:def 7;

            deffunc F( Nat) = (g - (((g - p) / k) * $1));

            consider s1 such that

             A78: for n be Nat holds (s1 . n) = F(n) from SEQ_1:sch 1;

            

             A79: 0 < ((g - p) / k) by A74, A76, A75, XREAL_1: 139;

             A80:

            now

              let n;

              

               A81: ( dom (f | [.p, g.])) = [.p, g.] by A2, RELAT_1: 62;

              assume

               A82: n < k;

              then (((g - p) / k) * n) < (((g - p) / k) * k) by A79, XREAL_1: 68;

              then (((g - p) / k) * n) < (g - p) by A76, A75, XCMPLX_1: 87;

              then (g - (g - p)) < (g - (((g - p) / k) * n)) by XREAL_1: 15;

              then

               A83: (g - (g - p)) < (s1 . n) by A78;

              (n + 1) <= k by A82, NAT_1: 13;

              then (((g - p) / k) * (n + 1)) <= (((g - p) / k) * k) by A74, XREAL_1: 64;

              then (((g - p) / k) * (n + 1)) <= (g - p) by A76, A75, XCMPLX_1: 87;

              then (g - (g - p)) <= (g - (((g - p) / k) * (n + 1))) by XREAL_1: 13;

              then

               A84: (g - (g - p)) <= (s1 . (n + 1)) by A78;

              (g - (((g - p) / k) * n)) <= (g - 0 ) by A74, XREAL_1: 13;

              then (s1 . n) <= g by A78;

              then (s1 . n) in { x2 : p <= x2 & x2 <= g } by A83;

              hence

               A85: (s1 . n) in [.p, g.] by RCOMP_1:def 1;

              (g - (((g - p) / k) * (n + 1))) <= (g - 0 ) by A74, XREAL_1: 13;

              then (s1 . (n + 1)) <= g by A78;

              then (s1 . (n + 1)) in { x2 : p <= x2 & x2 <= g } by A84;

              hence

               A86: (s1 . (n + 1)) in [.p, g.] by RCOMP_1:def 1;

               |.((s1 . (n + 1)) - (s1 . n)).| = |.((g - (((g - p) / k) * (n + 1))) - (s1 . n)).| by A78

              .= |.((g - (((g - p) / k) * (n + 1))) - (g - (((g - p) / k) * n))).| by A78

              .= |.( - ((((g - p) / k) * (n + 1)) - (((g - p) / k) * n))).|

              .= |.(((g - p) / k) * ((n + 1) - n)).| by COMPLEX1: 52

              .= ((g - p) / k) by A74, ABSVALUE:def 1;

              hence |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < (1 / ( |.M.| + 1)) by A68, A77, A85, A86, A81;

            end;

            defpred P[ Nat] means r <= (f . (s1 . $1));

            

             A87: (s1 . k) = (g - (((g - p) / k) * k)) by A78

            .= (g - (g - p)) by A76, A75, XCMPLX_1: 87

            .= p;

            then

             A88: ex n be Nat st P[n] by A54;

            consider l be Nat such that

             A89: P[l] & for m be Nat st P[m] holds l <= m from NAT_1:sch 5( A88);

            (s1 . 0 ) = (g - (((g - p) / k) * 0 )) by A78

            .= g;

            then l <> 0 by A54, A55, A89, XXREAL_0: 1;

            then

            consider l1 be Nat such that

             A90: l = (l1 + 1) by NAT_1: 6;

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

            

             A91: (r - (f . (s1 . l1))) <= ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) by A89, A90, XREAL_1: 9;

            (l1 + 1) <= k by A54, A87, A89, A90;

            then

             A92: l1 < k by NAT_1: 13;

            then

             A93: |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| < (1 / ( |.M.| + 1)) by A80;

            (f . (s1 . l1)) < r

            proof

              assume r <= (f . (s1 . l1));

              then l <= l1 by A89;

              then (l + 0 ) < l by A90, XREAL_1: 8;

              hence contradiction;

            end;

            then

             A94: 0 < (r - (f . (s1 . l1))) by XREAL_1: 50;

            then 0 < ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) by A89, A90, XREAL_1: 9;

            then |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| = ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) by ABSVALUE:def 1;

            then

             A95: |.(r - (f . (s1 . l1))).| <= |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| by A94, A91, ABSVALUE:def 1;

            (s1 . l1) in [.p, g.] by A80, A92;

            hence contradiction by A69, A95, A93, XXREAL_0: 2;

          end;

        end;

        hence contradiction;

      end;

      (f . p) = (f . g) implies ex s st s in [.p, g.] & r = (f . s)

      proof

        assume

         A96: (f . p) = (f . g);

        take p;

        thus p in [.p, g.] by A1, XXREAL_1: 1;

        ( [.(f . p), (f . g).] \/ [.(f . g), (f . p).]) = {(f . p)} by A96, XXREAL_1: 17;

        hence thesis by A4, TARSKI:def 1;

      end;

      hence thesis by A6, A51, XXREAL_0: 1;

    end;

    theorem :: FCONT_2:16

    

     Th16: p <= g & [.p, g.] c= ( dom f) & (f | [.p, g.]) is continuous implies for r st r in [.( lower_bound (f .: [.p, g.])), ( upper_bound (f .: [.p, g.])).] holds ex s st s in [.p, g.] & r = (f . s)

    proof

      assume that

       A1: p <= g and

       A2: [.p, g.] c= ( dom f) and

       A3: (f | [.p, g.]) is continuous;

       [.p, g.] is compact by RCOMP_1: 6;

      then

       A4: (f .: [.p, g.]) is real-bounded by A2, A3, FCONT_1: 29, RCOMP_1: 10;

      set ub = ( upper_bound (f .: [.p, g.]));

      set lb = ( lower_bound (f .: [.p, g.]));

       [.p, g.] <> {} by A1, XXREAL_1: 1;

      then

      consider x2,x1 be Real such that

       A5: x2 in [.p, g.] and

       A6: x1 in [.p, g.] and

       A7: (f . x2) = ub and

       A8: (f . x1) = lb by A2, A3, FCONT_1: 31, RCOMP_1: 6;

      reconsider x1, x2 as Real;

      let r such that

       A9: r in [.lb, ub.];

      (f . x1) in (f .: [.p, g.]) by A2, A6, FUNCT_1:def 6;

      then

       A10: [.lb, ub.] = ( [.lb, ub.] \/ [.ub, lb.]) by A4, SEQ_4: 11, XXREAL_1: 222;

      now

        per cases ;

          suppose

           A11: x1 <= x2;

          

           A12: [.x1, x2.] c= [.p, g.] by A5, A6, XXREAL_2:def 12;

          

           A13: [.x1, x2.] c= [.p, g.] by A5, A6, XXREAL_2:def 12;

          then (f | [.x1, x2.]) is continuous by A3, FCONT_1: 16;

          then

          consider s such that

           A14: s in [.x1, x2.] and

           A15: r = (f . s) by A2, A9, A7, A8, A10, A11, A12, Th15, XBOOLE_1: 1;

          take s;

          thus s in [.p, g.] & r = (f . s) by A13, A14, A15;

        end;

          suppose

           A16: x2 <= x1;

          

           A17: [.x2, x1.] c= [.p, g.] by A5, A6, XXREAL_2:def 12;

          

           A18: [.x2, x1.] c= [.p, g.] by A5, A6, XXREAL_2:def 12;

          then (f | [.x2, x1.]) is continuous by A3, FCONT_1: 16;

          then

          consider s such that

           A19: s in [.x2, x1.] and

           A20: r = (f . s) by A2, A9, A7, A8, A10, A16, A17, Th15, XBOOLE_1: 1;

          take s;

          thus s in [.p, g.] & r = (f . s) by A18, A19, A20;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_2:17

    

     Th17: f is one-to-one & [.p, g.] c= ( dom f) & p <= g & (f | [.p, g.]) is continuous implies (f | [.p, g.]) is increasing or (f | [.p, g.]) is decreasing

    proof

      

       A0: p is set by TARSKI: 1;

      assume that

       A1: f is one-to-one and

       A2: [.p, g.] c= ( dom f) and

       A3: p <= g and

       A4: (f | [.p, g.]) is continuous and

       A5: not (f | [.p, g.]) is increasing and

       A6: not (f | [.p, g.]) is decreasing;

      now

        per cases ;

          suppose p = g;

          then [.p, g.] = {p} by XXREAL_1: 17;

          hence contradiction by A6, A0, RFUNCT_2: 44;

        end;

          suppose

           A7: p <> g;

          

           A8: g in [.p, g.] by A3, XXREAL_1: 1;

          

           A9: p in [.p, g.] by A3, XXREAL_1: 1;

          then

           A10: (f . p) <> (f . g) by A1, A2, A7, A8, FUNCT_1:def 4;

          now

            per cases by A10, XXREAL_0: 1;

              suppose

               A11: (f . p) < (f . g);

              

               A12: for x1 st p <= x1 & x1 <= g holds (f . p) <= (f . x1) & (f . x1) <= (f . g)

              proof

                let x1;

                assume that

                 A13: p <= x1 and

                 A14: x1 <= g and

                 A15: not ((f . p) <= (f . x1) & (f . x1) <= (f . g));

                now

                  per cases by A15;

                    suppose

                     A16: (f . x1) < (f . p);

                    then (f . p) in { r : (f . x1) <= r & r <= (f . g) } by A11;

                    then (f . p) in [.(f . x1), (f . g).] by RCOMP_1:def 1;

                    then

                     A17: (f . p) in ( [.(f . x1), (f . g).] \/ [.(f . g), (f . x1).]) by XBOOLE_0:def 3;

                    x1 in { r : p <= r & r <= g } by A13, A14;

                    then

                     A18: x1 in [.p, g.] by RCOMP_1:def 1;

                    g in [.p, g.] by A3, XXREAL_1: 1;

                    then

                     A19: [.x1, g.] c= [.p, g.] by A18, XXREAL_2:def 12;

                    then (f | [.x1, g.]) is continuous by A4, FCONT_1: 16;

                    then

                    consider s such that

                     A20: s in [.x1, g.] and

                     A21: (f . s) = (f . p) by A2, A14, A19, A17, Th15, XBOOLE_1: 1;

                    s in { t : x1 <= t & t <= g } by A20, RCOMP_1:def 1;

                    then

                     A22: ex r st r = s & x1 <= r & r <= g;

                    

                     A23: x1 > p by A13, A16, XXREAL_0: 1;

                    s in [.p, g.] by A19, A20;

                    hence contradiction by A1, A2, A9, A23, A21, A22, FUNCT_1:def 4;

                  end;

                    suppose

                     A24: (f . g) < (f . x1);

                    then (f . g) in { r : (f . p) <= r & r <= (f . x1) } by A11;

                    then (f . g) in [.(f . p), (f . x1).] by RCOMP_1:def 1;

                    then

                     A25: (f . g) in ( [.(f . p), (f . x1).] \/ [.(f . x1), (f . p).]) by XBOOLE_0:def 3;

                    x1 in { r : p <= r & r <= g } by A13, A14;

                    then

                     A26: x1 in [.p, g.] by RCOMP_1:def 1;

                    p in [.p, g.] by A3, XXREAL_1: 1;

                    then

                     A27: [.p, x1.] c= [.p, g.] by A26, XXREAL_2:def 12;

                    then (f | [.p, x1.]) is continuous by A4, FCONT_1: 16;

                    then

                    consider s such that

                     A28: s in [.p, x1.] and

                     A29: (f . s) = (f . g) by A2, A13, A27, A25, Th15, XBOOLE_1: 1;

                    s in { t : p <= t & t <= x1 } by A28, RCOMP_1:def 1;

                    then

                     A30: ex r st r = s & p <= r & r <= x1;

                    s in [.p, g.] by A27, A28;

                    then s = g by A1, A2, A8, A29, FUNCT_1:def 4;

                    hence contradiction by A14, A24, A30, XXREAL_0: 1;

                  end;

                end;

                hence contradiction;

              end;

              consider x1, x2 such that

               A31: x1 in ( [.p, g.] /\ ( dom f)) and

               A32: x2 in ( [.p, g.] /\ ( dom f)) and

               A33: x1 < x2 and

               A34: (f . x2) <= (f . x1) by A5, RFUNCT_2: 20;

              

               A35: x1 in [.p, g.] by A31, XBOOLE_0:def 4;

              then

               A36: [.p, x1.] c= [.p, g.] by A9, XXREAL_2:def 12;

              

               A37: x2 in [.p, g.] by A32, XBOOLE_0:def 4;

              then x2 in { r : p <= r & r <= g } by RCOMP_1:def 1;

              then ex r st r = x2 & p <= r & r <= g;

              then (f . p) <= (f . x2) by A12;

              then (f . x2) in { r : (f . p) <= r & r <= (f . x1) } by A34;

              then (f . x2) in [.(f . p), (f . x1).] by RCOMP_1:def 1;

              then

               A38: (f . x2) in ( [.(f . p), (f . x1).] \/ [.(f . x1), (f . p).]) by XBOOLE_0:def 3;

              x1 in { t : p <= t & t <= g } by A35, RCOMP_1:def 1;

              then

               A39: ex r st r = x1 & p <= r & r <= g;

              p in [.p, g.] by A3, XXREAL_1: 1;

              then

               A40: [.p, x1.] c= [.p, g.] by A35, XXREAL_2:def 12;

              then (f | [.p, x1.]) is continuous by A4, FCONT_1: 16;

              then

              consider s such that

               A41: s in [.p, x1.] and

               A42: (f . s) = (f . x2) by A2, A39, A38, A36, Th15, XBOOLE_1: 1;

              s in { t : p <= t & t <= x1 } by A41, RCOMP_1:def 1;

              then

               A43: ex r st r = s & p <= r & r <= x1;

              s in [.p, g.] by A40, A41;

              hence contradiction by A1, A2, A33, A37, A42, A43, FUNCT_1:def 4;

            end;

              suppose

               A44: (f . p) > (f . g);

              

               A45: for x1 st p <= x1 & x1 <= g holds (f . g) <= (f . x1) & (f . x1) <= (f . p)

              proof

                let x1;

                assume that

                 A46: p <= x1 and

                 A47: x1 <= g and

                 A48: not ((f . g) <= (f . x1) & (f . x1) <= (f . p));

                now

                  per cases by A48;

                    suppose

                     A49: (f . x1) < (f . g);

                    now

                      per cases ;

                        suppose g = x1;

                        hence contradiction by A49;

                      end;

                        suppose

                         A50: g <> x1;

                        x1 in { r : p <= r & r <= g } by A46, A47;

                        then

                         A51: x1 in [.p, g.] by RCOMP_1:def 1;

                        (f . g) in { r : (f . x1) <= r & r <= (f . p) } by A44, A49;

                        then (f . g) in [.(f . x1), (f . p).] by RCOMP_1:def 1;

                        then

                         A52: (f . g) in ( [.(f . p), (f . x1).] \/ [.(f . x1), (f . p).]) by XBOOLE_0:def 3;

                        p in [.p, g.] by A3, XXREAL_1: 1;

                        then

                         A53: [.p, x1.] c= [.p, g.] by A51, XXREAL_2:def 12;

                        then (f | [.p, x1.]) is continuous by A4, FCONT_1: 16;

                        then

                        consider s such that

                         A54: s in [.p, x1.] and

                         A55: (f . s) = (f . g) by A2, A46, A53, A52, Th15, XBOOLE_1: 1;

                        s in { t : p <= t & t <= x1 } by A54, RCOMP_1:def 1;

                        then

                         A56: ex r st r = s & p <= r & r <= x1;

                        s in [.p, g.] by A53, A54;

                        then s = g by A1, A2, A8, A55, FUNCT_1:def 4;

                        hence contradiction by A47, A50, A56, XXREAL_0: 1;

                      end;

                    end;

                    hence contradiction;

                  end;

                    suppose

                     A57: (f . p) < (f . x1);

                    now

                      per cases ;

                        suppose p = x1;

                        hence contradiction by A57;

                      end;

                        suppose

                         A58: p <> x1;

                        x1 in { r : p <= r & r <= g } by A46, A47;

                        then

                         A59: x1 in [.p, g.] by RCOMP_1:def 1;

                        (f . p) in { r : (f . g) <= r & r <= (f . x1) } by A44, A57;

                        then (f . p) in [.(f . g), (f . x1).] by RCOMP_1:def 1;

                        then

                         A60: (f . p) in ( [.(f . x1), (f . g).] \/ [.(f . g), (f . x1).]) by XBOOLE_0:def 3;

                        g in [.p, g.] by A3, XXREAL_1: 1;

                        then

                         A61: [.x1, g.] c= [.p, g.] by A59, XXREAL_2:def 12;

                        then (f | [.x1, g.]) is continuous by A4, FCONT_1: 16;

                        then

                        consider s such that

                         A62: s in [.x1, g.] and

                         A63: (f . s) = (f . p) by A2, A47, A61, A60, Th15, XBOOLE_1: 1;

                        s in { t : x1 <= t & t <= g } by A62, RCOMP_1:def 1;

                        then

                         A64: ex r st r = s & x1 <= r & r <= g;

                        s in [.p, g.] by A61, A62;

                        then s = p by A1, A2, A9, A63, FUNCT_1:def 4;

                        hence contradiction by A46, A58, A64, XXREAL_0: 1;

                      end;

                    end;

                    hence contradiction;

                  end;

                end;

                hence contradiction;

              end;

              consider x1, x2 such that

               A65: x1 in ( [.p, g.] /\ ( dom f)) and

               A66: x2 in ( [.p, g.] /\ ( dom f)) and

               A67: x1 < x2 and

               A68: (f . x1) <= (f . x2) by A6, RFUNCT_2: 21;

              

               A69: x2 in [.p, g.] by A66, XBOOLE_0:def 4;

              then

               A70: [.x2, g.] c= [.p, g.] by A8, XXREAL_2:def 12;

              

               A71: x1 in [.p, g.] by A65, XBOOLE_0:def 4;

              then x1 in { t : p <= t & t <= g } by RCOMP_1:def 1;

              then ex r st r = x1 & p <= r & r <= g;

              then (f . g) <= (f . x1) by A45;

              then (f . x1) in { r : (f . g) <= r & r <= (f . x2) } by A68;

              then (f . x1) in [.(f . g), (f . x2).] by RCOMP_1:def 1;

              then

               A72: (f . x1) in ( [.(f . x2), (f . g).] \/ [.(f . g), (f . x2).]) by XBOOLE_0:def 3;

              x2 in { r : p <= r & r <= g } by A69, RCOMP_1:def 1;

              then

               A73: ex r st r = x2 & p <= r & r <= g;

              g in [.p, g.] by A3, XXREAL_1: 1;

              then

               A74: [.x2, g.] c= [.p, g.] by A69, XXREAL_2:def 12;

              then (f | [.x2, g.]) is continuous by A4, FCONT_1: 16;

              then

              consider s such that

               A75: s in [.x2, g.] and

               A76: (f . s) = (f . x1) by A2, A73, A72, A70, Th15, XBOOLE_1: 1;

              s in { t : x2 <= t & t <= g } by A75, RCOMP_1:def 1;

              then

               A77: ex r st r = s & x2 <= r & r <= g;

              s in [.p, g.] by A74, A75;

              hence contradiction by A1, A2, A67, A71, A76, A77, FUNCT_1:def 4;

            end;

          end;

          hence contradiction;

        end;

      end;

      hence contradiction;

    end;

    theorem :: FCONT_2:18

    f is one-to-one & p <= g & [.p, g.] c= ( dom f) & (f | [.p, g.]) is continuous implies ( lower_bound (f .: [.p, g.])) = (f . p) & ( upper_bound (f .: [.p, g.])) = (f . g) or ( lower_bound (f .: [.p, g.])) = (f . g) & ( upper_bound (f .: [.p, g.])) = (f . p)

    proof

      assume that

       A1: f is one-to-one and

       A2: p <= g and

       A3: [.p, g.] c= ( dom f) and

       A4: (f | [.p, g.]) is continuous;

      

       A5: p in [.p, g.] by A2, XXREAL_1: 1;

      then

       A6: (f . p) in (f .: [.p, g.]) by A3, FUNCT_1:def 6;

      

       A7: g in [.p, g.] by A2, XXREAL_1: 1;

      then

       A8: (f . g) in (f .: [.p, g.]) by A3, FUNCT_1:def 6;

      

       A9: g in ( [.p, g.] /\ ( dom f)) by A3, A7, XBOOLE_0:def 4;

      

       A10: p in ( [.p, g.] /\ ( dom f)) by A3, A5, XBOOLE_0:def 4;

       [.p, g.] <> {} by A2, XXREAL_1: 1;

      then

      consider x1,x2 be Real such that

       A11: x1 in [.p, g.] and

       A12: x2 in [.p, g.] and

       A13: (f . x1) = ( upper_bound (f .: [.p, g.])) and

       A14: (f . x2) = ( lower_bound (f .: [.p, g.])) by A3, A4, FCONT_1: 31, RCOMP_1: 6;

      

       A15: x2 in ( [.p, g.] /\ ( dom f)) by A3, A12, XBOOLE_0:def 4;

      x2 in { t : p <= t & t <= g } by A12, RCOMP_1:def 1;

      then

       A16: ex r st r = x2 & p <= r & r <= g;

      x1 in { r : p <= r & r <= g } by A11, RCOMP_1:def 1;

      then

       A17: ex r st r = x1 & p <= r & r <= g;

       [.p, g.] is compact by RCOMP_1: 6;

      then

       A18: (f .: [.p, g.]) is real-bounded by A3, A4, FCONT_1: 29, RCOMP_1: 10;

      

       A19: x1 in ( [.p, g.] /\ ( dom f)) by A3, A11, XBOOLE_0:def 4;

      now

        per cases by A1, A2, A3, A4, Th17;

          suppose

           A20: (f | [.p, g.]) is increasing;

           A21:

          now

            assume x1 <> g;

            then x1 < g by A17, XXREAL_0: 1;

            then (f . x1) < (f . g) by A9, A19, A20, RFUNCT_2: 20;

            hence contradiction by A8, A18, A13, SEQ_4:def 1;

          end;

          now

            assume x2 <> p;

            then p < x2 by A16, XXREAL_0: 1;

            then (f . p) < (f . x2) by A10, A15, A20, RFUNCT_2: 20;

            hence contradiction by A6, A18, A14, SEQ_4:def 2;

          end;

          hence thesis by A13, A14, A21;

        end;

          suppose

           A22: (f | [.p, g.]) is decreasing;

           A23:

          now

            assume x2 <> g;

            then x2 < g by A16, XXREAL_0: 1;

            then (f . g) < (f . x2) by A9, A15, A22, RFUNCT_2: 21;

            hence contradiction by A8, A18, A14, SEQ_4:def 2;

          end;

          now

            assume x1 <> p;

            then p < x1 by A17, XXREAL_0: 1;

            then (f . x1) < (f . p) by A10, A19, A22, RFUNCT_2: 21;

            hence contradiction by A6, A18, A13, SEQ_4:def 1;

          end;

          hence thesis by A13, A14, A23;

        end;

      end;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: FCONT_2:19

    

     Th19: p <= g & [.p, g.] c= ( dom f) & (f | [.p, g.]) is continuous implies (f .: [.p, g.]) = [.( lower_bound (f .: [.p, g.])), ( upper_bound (f .: [.p, g.])).]

    proof

      assume that

       A1: p <= g and

       A2: [.p, g.] c= ( dom f) and

       A3: (f | [.p, g.]) is continuous;

       [.p, g.] is compact by RCOMP_1: 6;

      then

       A4: (f .: [.p, g.]) is real-bounded by A2, A3, FCONT_1: 29, RCOMP_1: 10;

      now

        let y be Element of REAL ;

        thus y in (f .: [.p, g.]) implies y in [.( lower_bound (f .: [.p, g.])), ( upper_bound (f .: [.p, g.])).]

        proof

          assume

           A5: y in (f .: [.p, g.]);

          then

           A6: y >= ( lower_bound (f .: [.p, g.])) by A4, SEQ_4:def 2;

          y <= ( upper_bound (f .: [.p, g.])) by A4, A5, SEQ_4:def 1;

          then y in { s : ( lower_bound (f .: [.p, g.])) <= s & s <= ( upper_bound (f .: [.p, g.])) } by A6;

          hence thesis by RCOMP_1:def 1;

        end;

        assume y in [.( lower_bound (f .: [.p, g.])), ( upper_bound (f .: [.p, g.])).];

        then ex x0 st x0 in [.p, g.] & y = (f . x0) by A1, A2, A3, Th16;

        hence y in (f .: [.p, g.]) by A2, FUNCT_1:def 6;

      end;

      hence thesis by SUBSET_1: 3;

    end;

    theorem :: FCONT_2:20

    for f be one-to-one PartFunc of REAL , REAL st p <= g & [.p, g.] c= ( dom f) & (f | [.p, g.]) is continuous holds ((f " ) | [.( lower_bound (f .: [.p, g.])), ( upper_bound (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 continuous;

      now

        per cases by A1, A2, A3, Th17;

          suppose (f | [.p, g.]) is increasing;

          then (((f | [.p, g.]) " ) | (f .: [.p, g.])) is increasing by RFUNCT_2: 51;

          then (((f " ) | (f .: [.p, g.])) | (f .: [.p, g.])) is increasing by RFUNCT_2: 17;

          then ((f " ) | (f .: [.p, g.])) is monotone by RELAT_1: 72;

          then

           A4: ((f " ) | [.( lower_bound (f .: [.p, g.])), ( upper_bound (f .: [.p, g.])).]) is monotone by A1, A2, A3, Th19;

          ((f " ) .: [.( lower_bound (f .: [.p, g.])), ( upper_bound (f .: [.p, g.])).]) = ((f " ) .: (f .: [.p, g.])) by A1, A2, A3, Th19

          .= (((f " ) | (f .: [.p, g.])) .: (f .: [.p, g.])) by RELAT_1: 129

          .= (((f | [.p, g.]) " ) .: (f .: [.p, g.])) by RFUNCT_2: 17

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

          hence thesis by A1, A4, FCONT_1: 46;

        end;

          suppose (f | [.p, g.]) is decreasing;

          then (((f | [.p, g.]) " ) | (f .: [.p, g.])) is decreasing by RFUNCT_2: 52;

          then (((f " ) | (f .: [.p, g.])) | (f .: [.p, g.])) is decreasing by RFUNCT_2: 17;

          then ((f " ) | (f .: [.p, g.])) is monotone by RELAT_1: 72;

          then

           A5: ((f " ) | [.( lower_bound (f .: [.p, g.])), ( upper_bound (f .: [.p, g.])).]) is monotone by A1, A2, A3, Th19;

          ((f " ) .: [.( lower_bound (f .: [.p, g.])), ( upper_bound (f .: [.p, g.])).]) = ((f " ) .: (f .: [.p, g.])) by A1, A2, A3, Th19

          .= (((f " ) | (f .: [.p, g.])) .: (f .: [.p, g.])) by RELAT_1: 129

          .= (((f | [.p, g.]) " ) .: (f .: [.p, g.])) by RFUNCT_2: 17

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

          hence thesis by A1, A5, FCONT_1: 46;

        end;

      end;

      hence thesis;

    end;