fcont_3.miz



    begin

    reserve x,X for set;

    reserve x0,r1,r2,g,g1,g2,p,s for Real;

    reserve r for Real;

    reserve n,m for Nat;

    reserve a,b,d for Real_Sequence;

    reserve f for PartFunc of REAL , REAL ;

    registration

      cluster ( [#] REAL ) -> closed;

      coherence by XREAL_0:def 1;

      cluster empty -> closed for Subset of REAL ;

      coherence by XBOOLE_1: 3;

    end

    registration

      cluster ( [#] REAL ) -> open;

      coherence

      proof

        (( [#] REAL ) ` ) = ( {} REAL ) by XBOOLE_1: 37;

        hence thesis;

      end;

      cluster empty -> open for Subset of REAL ;

      coherence

      proof

        let S be Subset of REAL ;

        assume S is empty;

        then (S ` ) = ( [#] REAL );

        hence thesis;

      end;

    end

    registration

      let r;

      cluster ( right_closed_halfline r) -> closed;

      coherence

      proof

        set b = ( seq_const r);

        let a such that

         A1: ( rng a) c= ( right_closed_halfline r) and

         A2: a is convergent;

         A3:

        now

          let n;

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

          then (a . n) in ( right_closed_halfline r) by A1;

          then (a . n) in { g1 : r <= g1 } by XXREAL_1: 232;

          then ex r1 st (a . n) = r1 & r <= r1;

          hence (b . n) <= (a . n) by SEQ_1: 57;

        end;

        ( lim b) = (b . 0 ) by SEQ_4: 26

        .= r by SEQ_1: 57;

        then r <= ( lim a) by A2, A3, SEQ_2: 18;

        then ( lim a) in { g1 : r <= g1 };

        hence thesis by XXREAL_1: 232;

      end;

      cluster ( left_closed_halfline r) -> closed;

      coherence

      proof

        set b = ( seq_const r);

        let a such that

         A4: ( rng a) c= ( left_closed_halfline r) and

         A5: a is convergent;

         A6:

        now

          let n;

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

          then (a . n) in ( left_closed_halfline r) by A4;

          then (a . n) in { g : g <= r } by XXREAL_1: 231;

          then ex r1 st (a . n) = r1 & r1 <= r;

          hence (a . n) <= (b . n) by SEQ_1: 57;

        end;

        ( lim b) = (b . 0 ) by SEQ_4: 26

        .= r by SEQ_1: 57;

        then ( lim a) <= r by A5, A6, SEQ_2: 18;

        then ( lim a) in { g1 : g1 <= r };

        hence thesis by XXREAL_1: 231;

      end;

      cluster ( right_open_halfline r) -> open;

      coherence

      proof

        (( right_open_halfline r) ` ) = ( left_closed_halfline r) by XXREAL_1: 224, XXREAL_1: 296;

        hence thesis;

      end;

      cluster ( halfline r) -> open;

      coherence

      proof

        (( left_open_halfline r) ` ) = ( right_closed_halfline r) by XXREAL_1: 224, XXREAL_1: 290;

        hence thesis;

      end;

    end

    theorem :: FCONT_3:1

    

     Th1: g in ].(x0 - r), (x0 + r).[ implies |.(g - x0).| < r

    proof

      assume g in ].(x0 - r), (x0 + r).[;

      then

       A1: ex g1 st g1 = g & (x0 - r) < g1 & g1 < (x0 + r);

      per cases ;

        suppose

         A2: x0 <= g;

        

         A3: (g - x0) < ((x0 + r) - x0) by A1, XREAL_1: 14;

         0 <= (g - x0) by A2, XREAL_1: 48;

        hence thesis by A3, ABSVALUE:def 1;

      end;

        suppose g <= x0;

        then 0 <= (x0 - g) by XREAL_1: 48;

        

        then

         A4: (x0 - g) = |.( - (g - x0)).| by ABSVALUE:def 1

        .= |.(g - x0).| by COMPLEX1: 52;

        (x0 - g) < (x0 - (x0 - r)) by A1, XREAL_1: 15;

        hence thesis by A4;

      end;

    end;

    theorem :: FCONT_3:2

    g in ].(x0 - r), (x0 + r).[ implies (g - x0) in ].( - r), r.[

    proof

      set r1 = (g - x0);

      assume g in ].(x0 - r), (x0 + r).[;

      then |.(g - x0).| < r by Th1;

      then |.(r1 - 0 ).| < r;

      then r1 in ].( 0 - r), ( 0 + r).[ by RCOMP_1: 1;

      hence thesis;

    end;

    theorem :: FCONT_3:3

    

     Th3: g = (x0 + r1) & |.r1.| < r implies 0 < r & g in ].(x0 - r), (x0 + r).[

    proof

      assume that

       A1: g = (x0 + r1) and

       A2: |.r1.| < r;

      thus 0 < r by A2, COMPLEX1: 46;

       |.(g - x0).| < r by A1, A2;

      hence thesis by RCOMP_1: 1;

    end;

    theorem :: FCONT_3:4

    (g - x0) in ].( - r), r.[ implies 0 < r & g in ].(x0 - r), (x0 + r).[

    proof

      set r1 = (g - x0);

      assume r1 in ].( - r), r.[;

      then ex g1 st g1 = r1 & ( - r) < g1 & g1 < r;

      then

       A1: |.r1.| < r by SEQ_2: 1;

      (x0 + r1) = g;

      hence thesis by A1, Th3;

    end;

    theorem :: FCONT_3:5

    

     Th5: for x0 be Real holds (for n holds (a . n) = (x0 - (p / (n + 1)))) implies a is convergent & ( lim a) = x0

    proof

      let x0 be Real;

      deffunc F( Nat) = (p / ($1 + 1));

      consider d such that

       A1: for n holds (d . n) = F(n) from SEQ_1:sch 1;

      set b = ( seq_const x0);

      assume

       A2: for n holds (a . n) = (x0 - (p / (n + 1)));

      now

        let n be Element of NAT ;

        

        thus ((b - d) . n) = ((b . n) - (d . n)) by VALUED_1: 15

        .= (x0 - (d . n)) by SEQ_1: 57

        .= (x0 - (p / (n + 1))) by A1

        .= (a . n) by A2;

      end;

      then

       A3: a = (b - d) by FUNCT_2: 63;

      

       A4: d is convergent by A1, SEQ_4: 31;

      hence a is convergent by A3;

      

       A5: ( lim b) = (b . 0 ) by SEQ_4: 26

      .= x0 by SEQ_1: 57;

      ( lim d) = 0 by A1, SEQ_4: 31;

      

      hence ( lim a) = (x0 - 0 ) by A4, A5, A3, SEQ_2: 12

      .= x0;

    end;

    theorem :: FCONT_3:6

    

     Th6: for x0 be Real holds (for n holds (a . n) = (x0 + (p / (n + 1)))) implies a is convergent & ( lim a) = x0

    proof

      let x0 be Real;

      deffunc F( Nat) = (p / ($1 + 1));

      consider d such that

       A1: for n holds (d . n) = F(n) from SEQ_1:sch 1;

      set b = ( seq_const x0);

      assume

       A2: for n holds (a . n) = (x0 + (p / (n + 1)));

      now

        let n be Element of NAT ;

        

        thus ((b + d) . n) = ((b . n) + (d . n)) by VALUED_1: 1

        .= (x0 + (d . n)) by SEQ_1: 57

        .= (x0 + (p / (n + 1))) by A1

        .= (a . n) by A2;

      end;

      then

       A3: a = (b + d) by FUNCT_2: 63;

      

       A4: d is convergent by A1, SEQ_4: 31;

      hence a is convergent by A3;

      

       A5: ( lim b) = (b . 0 ) by SEQ_4: 26

      .= x0 by SEQ_1: 57;

      ( lim d) = 0 by A1, SEQ_4: 31;

      

      hence ( lim a) = (x0 + 0 ) by A4, A5, A3, SEQ_2: 6

      .= x0;

    end;

    theorem :: FCONT_3:7

    f is_continuous_in x0 & (f . x0) <> r & (ex N be Neighbourhood of x0 st N c= ( dom f)) implies ex N be Neighbourhood of x0 st N c= ( dom f) & for g st g in N holds (f . g) <> r

    proof

      assume that

       A1: f is_continuous_in x0 and

       A2: (f . x0) <> r;

      given N be Neighbourhood of x0 such that

       A3: N c= ( dom f);

      consider p be Real such that

       A4: 0 < p and

       A5: N = ].(x0 - p), (x0 + p).[ by RCOMP_1:def 6;

      defpred P[ Nat, Real] means (x0 - (p / ($1 + 1))) < $2 & $2 < (x0 + (p / ($1 + 1))) & (f . $2) = r & $2 in ( dom f);

      assume

       A6: for N be Neighbourhood of x0 holds not N c= ( dom f) or ex g st g in N & (f . g) = r;

      

       A7: for n be Element of NAT holds ex g be Element of REAL st P[n, g]

      proof

        let n be Element of NAT ;

        

         A8: 0 <= n by NAT_1: 2;

        then

        reconsider Nn = ].(x0 - (p / (n + 1))), (x0 + (p / (n + 1))).[ as Neighbourhood of x0 by A4, RCOMP_1:def 6, XREAL_1: 139;

        

         A9: Nn c= ( dom f)

        proof

          let x be object;

          assume x in Nn;

          then

          consider g2 such that

           A10: g2 = x and

           A11: (x0 - (p / (n + 1))) < g2 and

           A12: g2 < (x0 + (p / (n + 1)));

          ( 0 + 1) <= (n + 1) by A8, XREAL_1: 7;

          then

           A13: (p / (n + 1)) <= (p / 1) by A4, XREAL_1: 118;

          then (x0 + (p / (n + 1))) <= (x0 + p) by XREAL_1: 7;

          then

           A14: g2 < (x0 + p) by A12, XXREAL_0: 2;

          (x0 - p) <= (x0 - (p / (n + 1))) by A13, XREAL_1: 13;

          then (x0 - p) < g2 by A11, XXREAL_0: 2;

          then x in N by A5, A10, A14;

          hence thesis by A3;

        end;

        then

        consider g such that

         A15: g in Nn and

         A16: (f . g) = r by A6;

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

        take g;

        ex g1 st g1 = g & (x0 - (p / (n + 1))) < g1 & g1 < (x0 + (p / (n + 1))) by A15;

        hence (x0 - (p / (n + 1))) < g & g < (x0 + (p / (n + 1)));

        thus (f . g) = r by A16;

        thus thesis by A9, A15;

      end;

      consider d such that

       A17: for n be Element of NAT holds P[n, (d . n)] from FUNCT_2:sch 3( A7);

      

       A18: ( rng d) c= ( dom f)

      proof

        let x be object;

        assume x in ( rng d);

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

        hence thesis by A17;

      end;

       A19:

      now

        let r2 be Real such that

         A20: 0 < r2;

        reconsider n = 0 as Nat;

        take n;

        let m be Nat such that n <= m;

        

         A21: m in NAT by ORDINAL1:def 12;

         |.(((f /* d) . m) - r).| = |.((f . (d . m)) - r).| by A18, FUNCT_2: 108, A21

        .= |.(r - r).| by A17, A21

        .= 0 by ABSVALUE: 2;

        hence |.(((f /* d) . m) - r).| < r2 by A20;

      end;

      deffunc F( Nat) = (x0 - (p / ($1 + 1)));

      consider a such that

       A22: for n holds (a . n) = F(n) from SEQ_1:sch 1;

      deffunc F( Nat) = (x0 + (p / ($1 + 1)));

      consider b such that

       A23: for n holds (b . n) = F(n) from SEQ_1:sch 1;

       A24:

      now

        let n;

        n in NAT by ORDINAL1:def 12;

        then (x0 - (p / (n + 1))) < (d . n) & (d . n) < (x0 + (p / (n + 1))) by A17;

        hence (a . n) <= (d . n) & (d . n) <= (b . n) by A22, A23;

      end;

      

       A25: b is convergent & ( lim b) = x0 by A23, Th6;

      a is convergent & ( lim a) = x0 by A22, Th5;

      then d is convergent & ( lim d) = x0 by A25, A24, SEQ_2: 19, SEQ_2: 20;

      then (f /* d) is convergent & (f . x0) = ( lim (f /* d)) by A1, A18, FCONT_1:def 1;

      hence contradiction by A2, A19, SEQ_2:def 7;

    end;

    theorem :: FCONT_3:8

    (f | X) is increasing or (f | X) is decreasing implies (f | X) is one-to-one

    proof

      assume

       A1: (f | X) is increasing or (f | X) is decreasing;

      now

        per cases by A1;

          suppose

           A2: (f | X) is increasing;

          now

            given r1,r2 be Element of REAL such that

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

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

             A5: ((f | X) . r1) = ((f | X) . r2) and

             A6: r1 <> r2;

            

             A7: r1 in (X /\ ( dom f)) & r2 in (X /\ ( dom f)) by A3, A4, RELAT_1: 61;

            now

              per cases by A6, XXREAL_0: 1;

                suppose r1 < r2;

                then (f . r1) < (f . r2) by A2, A7, RFUNCT_2: 20;

                then ((f | X) . r1) < (f . r2) by A3, FUNCT_1: 47;

                hence contradiction by A4, A5, FUNCT_1: 47;

              end;

                suppose r2 < r1;

                then (f . r2) < (f . r1) by A2, A7, RFUNCT_2: 20;

                then ((f | X) . r2) < (f . r1) by A4, FUNCT_1: 47;

                hence contradiction by A3, A5, FUNCT_1: 47;

              end;

            end;

            hence contradiction;

          end;

          hence thesis by PARTFUN1: 8;

        end;

          suppose

           A8: (f | X) is decreasing;

          now

            given r1,r2 be Element of REAL such that

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

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

             A11: ((f | X) . r1) = ((f | X) . r2) and

             A12: r1 <> r2;

            

             A13: r1 in (X /\ ( dom f)) & r2 in (X /\ ( dom f)) by A9, A10, RELAT_1: 61;

            now

              per cases by A12, XXREAL_0: 1;

                suppose r1 < r2;

                then (f . r2) < (f . r1) by A8, A13, RFUNCT_2: 21;

                then ((f | X) . r2) < (f . r1) by A10, FUNCT_1: 47;

                hence contradiction by A9, A11, FUNCT_1: 47;

              end;

                suppose r2 < r1;

                then (f . r1) < (f . r2) by A8, A13, RFUNCT_2: 21;

                then ((f | X) . r1) < (f . r2) by A9, FUNCT_1: 47;

                hence contradiction by A10, A11, FUNCT_1: 47;

              end;

            end;

            hence contradiction;

          end;

          hence thesis by PARTFUN1: 8;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_3:9

    

     Th9: for f be one-to-one PartFunc of REAL , REAL st (f | X) is increasing holds (((f | X) " ) | (f .: X)) is increasing

    proof

      let f be one-to-one PartFunc of REAL , REAL ;

      assume that

       A1: (f | X) is increasing and

       A2: not (((f | X) " ) | (f .: X)) is increasing;

      consider r1, r2 such that

       A3: r1 in ((f .: X) /\ ( dom ((f | X) " ))) and

       A4: r2 in ((f .: X) /\ ( dom ((f | X) " ))) and

       A5: r1 < r2 and

       A6: (((f | X) " ) . r1) >= (((f | X) " ) . r2) by A2, RFUNCT_2: 20;

      

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

      then

       A8: r1 in ( rng (f | X)) by A3, XBOOLE_0:def 4;

      

       A9: r2 in ( rng (f | X)) by A4, A7, XBOOLE_0:def 4;

      

       A10: ((f | X) | X) is increasing by A1;

      now

        per cases ;

          suppose (((f | X) " ) . r1) = (((f | X) " ) . r2);

          

          then r1 = ((f | X) . (((f | X) " ) . r2)) by A8, FUNCT_1: 35

          .= r2 by A9, FUNCT_1: 35;

          hence contradiction by A5;

        end;

          suppose

           A11: (((f | X) " ) . r1) <> (((f | X) " ) . r2);

          

           A12: ( dom (f | X)) = ( dom ((f | X) | X))

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

          r1 in REAL & r2 in REAL & (((f | X) " ) . r2) in REAL & (((f | X) " ) . r1) in REAL by XREAL_0:def 1;

          then

           A13: (((f | X) " ) . r2) in ( dom (f | X)) & (((f | X) " ) . r1) in ( dom (f | X)) by A8, A9, PARTFUN2: 60;

          (((f | X) " ) . r2) < (((f | X) " ) . r1) by A6, A11, XXREAL_0: 1;

          then ((f | X) . (((f | X) " ) . r2)) < ((f | X) . (((f | X) " ) . r1)) by A10, A13, A12, RFUNCT_2: 20;

          then r2 < ((f | X) . (((f | X) " ) . r1)) by A9, FUNCT_1: 35;

          hence contradiction by A5, A8, FUNCT_1: 35;

        end;

      end;

      hence contradiction;

    end;

    theorem :: FCONT_3:10

    

     Th10: for f be one-to-one PartFunc of REAL , REAL st (f | X) is decreasing holds (((f | X) " ) | (f .: X)) is decreasing

    proof

      let f be one-to-one PartFunc of REAL , REAL ;

      assume that

       A1: (f | X) is decreasing and

       A2: not (((f | X) " ) | (f .: X)) is decreasing;

      consider r1, r2 such that

       A3: r1 in ((f .: X) /\ ( dom ((f | X) " ))) and

       A4: r2 in ((f .: X) /\ ( dom ((f | X) " ))) and

       A5: r1 < r2 and

       A6: (((f | X) " ) . r1) <= (((f | X) " ) . r2) by A2, RFUNCT_2: 21;

      

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

      then

       A8: r1 in ( rng (f | X)) by A3, XBOOLE_0:def 4;

      

       A9: r2 in ( rng (f | X)) by A4, A7, XBOOLE_0:def 4;

      

       A10: ((f | X) | X) is decreasing by A1;

      now

        per cases ;

          suppose (((f | X) " ) . r1) = (((f | X) " ) . r2);

          

          then r1 = ((f | X) . (((f | X) " ) . r2)) by A8, FUNCT_1: 35

          .= r2 by A9, FUNCT_1: 35;

          hence contradiction by A5;

        end;

          suppose

           A11: (((f | X) " ) . r1) <> (((f | X) " ) . r2);

          

           A12: ( dom (f | X)) = ( dom ((f | X) | X))

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

          r1 in REAL & r2 in REAL & (((f | X) " ) . r2) in REAL & (((f | X) " ) . r1) in REAL by XREAL_0:def 1;

          then

           A13: (((f | X) " ) . r2) in ( dom (f | X)) & (((f | X) " ) . r1) in ( dom (f | X)) by A8, A9, PARTFUN2: 60;

          (((f | X) " ) . r2) > (((f | X) " ) . r1) by A6, A11, XXREAL_0: 1;

          then ((f | X) . (((f | X) " ) . r2)) < ((f | X) . (((f | X) " ) . r1)) by A10, A13, A12, RFUNCT_2: 21;

          then r2 < ((f | X) . (((f | X) " ) . r1)) by A9, FUNCT_1: 35;

          hence contradiction by A5, A8, FUNCT_1: 35;

        end;

      end;

      hence contradiction;

    end;

    theorem :: FCONT_3:11

    

     Th11: X c= ( dom f) & (f | X) is monotone & (ex p st (f .: X) = ( left_open_halfline p)) implies (f | X) is continuous

    proof

      assume that

       A1: X c= ( dom f) and

       A2: (f | X) is monotone;

      given p such that

       A3: (f .: X) = ( left_open_halfline p);

      set L = ( left_open_halfline p);

      now

        per cases by A2, RFUNCT_2:def 5;

          suppose (f | X) is non-decreasing;

          then

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

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

          proof

            let x0 be Real;

            

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

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

            then x0 in X;

            then x0 in (( dom f) /\ X) by A1, XBOOLE_0:def 4;

            then

             A6: x0 in ( dom (f | X)) by RELAT_1: 61;

            then ((f | X) . x0) in ((f | X) .: X) by FUNCT_1:def 6;

            then

             A7: ((f | X) . x0) in L by A3, RELAT_1: 129;

            now

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

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

               A8: N2 c= L by A7, RCOMP_1: 18;

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

               A9: N3 c= N1 and

               A10: N3 c= N2 by RCOMP_1: 17;

              consider r be Real such that

               A11: r > 0 and

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

              reconsider r as Real;

              

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

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

              

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

              

               A15: ((f | X) . x0) < (((f | X) . x0) + r) by A11, 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 A14, XXREAL_0: 2;

              then

               A16: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A13;

              then M2 in N2 by A10, A12;

              then

              consider r2 be Element of REAL such that

               A17: r2 in ( dom (f | X)) & r2 in X and

               A18: M2 = ((f | X) . r2) by A3, A5, A8, PARTFUN2: 59;

              

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

               A20:

              now

                assume

                 A21: r2 < x0;

                x0 in (X /\ ( dom (f | X))) & r2 in (X /\ ( dom (f | X))) by A6, A17, XBOOLE_0:def 4;

                hence contradiction by A4, A18, A19, A21, RFUNCT_2: 22;

              end;

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

              

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

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

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

              then

               A23: M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A22;

              then M1 in N2 by A10, A12;

              then

              consider r1 be Element of REAL such that

               A24: r1 in ( dom (f | X)) & r1 in X and

               A25: M1 = ((f | X) . r1) by A3, A5, A8, PARTFUN2: 59;

              

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

              then

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

               A28:

              now

                assume

                 A29: x0 < r1;

                x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A6, A24, XBOOLE_0:def 4;

                hence contradiction by A4, A25, A27, A29, RFUNCT_2: 22;

              end;

              x0 <> r2 by A11, A18, XREAL_1: 29, XREAL_1: 215;

              then x0 < r2 by A20, XXREAL_0: 1;

              then

               A30: (r2 - x0) > 0 by XREAL_1: 50;

              set R = ( min ((x0 - r1),(r2 - x0)));

              

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

              r1 <> x0 by A25, A26, XREAL_1: 19;

              then r1 < x0 by A28, XXREAL_0: 1;

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

              then R > 0 by A30, 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

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

               A33: x in N;

              

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

              

               A35: ex s st s = x & (x0 - R) < s & s < (x0 + R) by A33;

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

              then

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

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

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

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

              then

               A37: ((x - x0) + x0) > ((r1 - x0) + x0) by XREAL_1: 6;

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

              then

               A38: ((f | X) . r1) <= ((f | X) . x) by A4, A37, A34, RFUNCT_2: 22;

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

              then (x - x0) < (r2 - x0) by A31, XXREAL_0: 2;

              then

               A39: ((x - x0) + x0) < ((r2 - x0) + x0) by XREAL_1: 6;

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

              then ((f | X) . x) <= ((f | X) . r2) by A4, A39, A34, RFUNCT_2: 22;

              then

               A40: ((f | X) . x) in [.M1, M2.] by A25, A18, A38;

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

              then ((f | X) . x) in N3 by A12, A40;

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

            end;

            hence thesis by FCONT_1: 4;

          end;

          hence thesis by FCONT_1:def 2;

        end;

          suppose (f | X) is non-increasing;

          then

           A41: ((f | X) | X) is non-increasing;

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

          proof

            let x0 be Real;

            

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

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

            then x0 in X;

            then x0 in (( dom f) /\ X) by A1, XBOOLE_0:def 4;

            then

             A43: x0 in ( dom (f | X)) by RELAT_1: 61;

            then ((f | X) . x0) in ((f | X) .: X) by FUNCT_1:def 6;

            then

             A44: ((f | X) . x0) in L by A3, RELAT_1: 129;

            now

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

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

               A45: N2 c= L by A44, RCOMP_1: 18;

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

               A46: N3 c= N1 and

               A47: N3 c= N2 by RCOMP_1: 17;

              consider r be Real such that

               A48: r > 0 and

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

              reconsider r as Real;

              

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

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

              

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

              

               A52: ((f | X) . x0) < (((f | X) . x0) + r) by A48, 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 A51, XXREAL_0: 2;

              then

               A53: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A50;

              then M2 in N2 by A47, A49;

              then

              consider r2 be Element of REAL such that

               A54: r2 in ( dom (f | X)) & r2 in X and

               A55: M2 = ((f | X) . r2) by A3, A42, A45, PARTFUN2: 59;

              

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

               A57:

              now

                assume

                 A58: r2 > x0;

                x0 in (X /\ ( dom (f | X))) & r2 in (X /\ ( dom (f | X))) by A43, A54, XBOOLE_0:def 4;

                hence contradiction by A41, A55, A56, A58, RFUNCT_2: 23;

              end;

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

              

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

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

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

              then

               A60: M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A59;

              then M1 in N2 by A47, A49;

              then

              consider r1 be Element of REAL such that

               A61: r1 in ( dom (f | X)) & r1 in X and

               A62: M1 = ((f | X) . r1) by A3, A42, A45, PARTFUN2: 59;

              

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

              then

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

               A65:

              now

                assume

                 A66: x0 > r1;

                x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A43, A61, XBOOLE_0:def 4;

                hence contradiction by A41, A62, A64, A66, RFUNCT_2: 23;

              end;

              x0 <> r2 by A48, A55, XREAL_1: 29, XREAL_1: 215;

              then x0 > r2 by A57, XXREAL_0: 1;

              then

               A67: (x0 - r2) > 0 by XREAL_1: 50;

              set R = ( min ((r1 - x0),(x0 - r2)));

              

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

              r1 <> x0 by A62, A63, XREAL_1: 19;

              then r1 > x0 by A65, XXREAL_0: 1;

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

              then R > 0 by A67, 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

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

               A70: x in N;

              

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

              

               A72: ex s st s = x & (x0 - R) < s & s < (x0 + R) by A70;

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

              then

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

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

              then (x - x0) < (r1 - x0) by A68, XXREAL_0: 2;

              then

               A74: ((x - x0) + x0) < ((r1 - x0) + x0) by XREAL_1: 6;

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

              then

               A75: ((f | X) . r1) <= ((f | X) . x) by A41, A74, A71, RFUNCT_2: 23;

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

              then (x0 - x) < (x0 - r2) by A73, XXREAL_0: 2;

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

              then

               A76: ((x - x0) + x0) > ((r2 - x0) + x0) by XREAL_1: 6;

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

              then ((f | X) . x) <= ((f | X) . r2) by A41, A76, A71, RFUNCT_2: 23;

              then

               A77: ((f | X) . x) in [.M1, M2.] by A62, A55, A75;

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

              then ((f | X) . x) in N3 by A49, A77;

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

            end;

            hence thesis by FCONT_1: 4;

          end;

          hence thesis by FCONT_1:def 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_3:12

    

     Th12: X c= ( dom f) & (f | X) is monotone & (ex p st (f .: X) = ( right_open_halfline p)) implies (f | X) is continuous

    proof

      assume that

       A1: X c= ( dom f) and

       A2: (f | X) is monotone;

      given p such that

       A3: (f .: X) = ( right_open_halfline p);

      set L = ( right_open_halfline p);

      now

        per cases by A2, RFUNCT_2:def 5;

          suppose (f | X) is non-decreasing;

          then

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

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

          proof

            let x0 be Real;

            

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

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

            then x0 in X;

            then x0 in (( dom f) /\ X) by A1, XBOOLE_0:def 4;

            then

             A6: x0 in ( dom (f | X)) by RELAT_1: 61;

            then ((f | X) . x0) in ((f | X) .: X) by FUNCT_1:def 6;

            then

             A7: ((f | X) . x0) in L by A3, RELAT_1: 129;

            now

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

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

               A8: N2 c= L by A7, RCOMP_1: 18;

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

               A9: N3 c= N1 and

               A10: N3 c= N2 by RCOMP_1: 17;

              consider r be Real such that

               A11: r > 0 and

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

              reconsider r as Real;

              

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

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

              

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

              

               A15: ((f | X) . x0) < (((f | X) . x0) + r) by A11, 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 A14, XXREAL_0: 2;

              then

               A16: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A13;

              then M2 in N2 by A10, A12;

              then

              consider r2 be Element of REAL such that

               A17: r2 in ( dom (f | X)) & r2 in X and

               A18: M2 = ((f | X) . r2) by A3, A5, A8, PARTFUN2: 59;

              

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

               A20:

              now

                assume

                 A21: r2 < x0;

                x0 in (X /\ ( dom (f | X))) & r2 in (X /\ ( dom (f | X))) by A6, A17, XBOOLE_0:def 4;

                hence contradiction by A4, A18, A19, A21, RFUNCT_2: 22;

              end;

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

              

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

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

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

              then

               A23: M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A22;

              then M1 in N2 by A10, A12;

              then

              consider r1 be Element of REAL such that

               A24: r1 in ( dom (f | X)) & r1 in X and

               A25: M1 = ((f | X) . r1) by A3, A5, A8, PARTFUN2: 59;

              

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

              then

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

               A28:

              now

                assume

                 A29: x0 < r1;

                x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A6, A24, XBOOLE_0:def 4;

                hence contradiction by A4, A25, A27, A29, RFUNCT_2: 22;

              end;

              x0 <> r2 by A11, A18, XREAL_1: 29, XREAL_1: 215;

              then x0 < r2 by A20, XXREAL_0: 1;

              then

               A30: (r2 - x0) > 0 by XREAL_1: 50;

              set R = ( min ((x0 - r1),(r2 - x0)));

              

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

              r1 <> x0 by A25, A26, XREAL_1: 19;

              then r1 < x0 by A28, XXREAL_0: 1;

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

              then R > 0 by A30, 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

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

               A33: x in N;

              

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

              

               A35: ex s st s = x & (x0 - R) < s & s < (x0 + R) by A33;

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

              then

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

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

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

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

              then

               A37: ((x - x0) + x0) > ((r1 - x0) + x0) by XREAL_1: 6;

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

              then

               A38: ((f | X) . r1) <= ((f | X) . x) by A4, A37, A34, RFUNCT_2: 22;

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

              then (x - x0) < (r2 - x0) by A31, XXREAL_0: 2;

              then

               A39: ((x - x0) + x0) < ((r2 - x0) + x0) by XREAL_1: 6;

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

              then ((f | X) . x) <= ((f | X) . r2) by A4, A39, A34, RFUNCT_2: 22;

              then

               A40: ((f | X) . x) in [.M1, M2.] by A25, A18, A38;

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

              then ((f | X) . x) in N3 by A12, A40;

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

            end;

            hence thesis by FCONT_1: 4;

          end;

          hence thesis by FCONT_1:def 2;

        end;

          suppose (f | X) is non-increasing;

          then

           A41: ((f | X) | X) is non-increasing;

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

          proof

            let x0 be Real;

            

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

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

            then x0 in X;

            then x0 in (( dom f) /\ X) by A1, XBOOLE_0:def 4;

            then

             A43: x0 in ( dom (f | X)) by RELAT_1: 61;

            then ((f | X) . x0) in ((f | X) .: X) by FUNCT_1:def 6;

            then

             A44: ((f | X) . x0) in L by A3, RELAT_1: 129;

            now

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

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

               A45: N2 c= L by A44, RCOMP_1: 18;

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

               A46: N3 c= N1 and

               A47: N3 c= N2 by RCOMP_1: 17;

              consider r be Real such that

               A48: r > 0 and

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

              reconsider r as Real;

              

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

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

              

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

              

               A52: ((f | X) . x0) < (((f | X) . x0) + r) by A48, 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 A51, XXREAL_0: 2;

              then

               A53: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A50;

              then M2 in N2 by A47, A49;

              then

              consider r2 be Element of REAL such that

               A54: r2 in ( dom (f | X)) & r2 in X and

               A55: M2 = ((f | X) . r2) by A3, A42, A45, PARTFUN2: 59;

              

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

               A57:

              now

                assume

                 A58: r2 > x0;

                x0 in (X /\ ( dom (f | X))) & r2 in (X /\ ( dom (f | X))) by A43, A54, XBOOLE_0:def 4;

                hence contradiction by A41, A55, A56, A58, RFUNCT_2: 23;

              end;

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

              

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

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

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

              then

               A60: M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A59;

              then M1 in N2 by A47, A49;

              then

              consider r1 be Element of REAL such that

               A61: r1 in ( dom (f | X)) & r1 in X and

               A62: M1 = ((f | X) . r1) by A3, A42, A45, PARTFUN2: 59;

              

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

              then

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

               A65:

              now

                assume

                 A66: x0 > r1;

                x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A43, A61, XBOOLE_0:def 4;

                hence contradiction by A41, A62, A64, A66, RFUNCT_2: 23;

              end;

              x0 <> r2 by A48, A55, XREAL_1: 29, XREAL_1: 215;

              then x0 > r2 by A57, XXREAL_0: 1;

              then

               A67: (x0 - r2) > 0 by XREAL_1: 50;

              set R = ( min ((r1 - x0),(x0 - r2)));

              

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

              r1 <> x0 by A62, A63, XREAL_1: 19;

              then r1 > x0 by A65, XXREAL_0: 1;

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

              then R > 0 by A67, 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

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

               A70: x in N;

              

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

              

               A72: ex s st s = x & (x0 - R) < s & s < (x0 + R) by A70;

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

              then

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

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

              then (x - x0) < (r1 - x0) by A68, XXREAL_0: 2;

              then

               A74: ((x - x0) + x0) < ((r1 - x0) + x0) by XREAL_1: 6;

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

              then

               A75: ((f | X) . r1) <= ((f | X) . x) by A41, A74, A71, RFUNCT_2: 23;

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

              then (x0 - x) < (x0 - r2) by A73, XXREAL_0: 2;

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

              then

               A76: ((x - x0) + x0) > ((r2 - x0) + x0) by XREAL_1: 6;

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

              then ((f | X) . x) <= ((f | X) . r2) by A41, A76, A71, RFUNCT_2: 23;

              then

               A77: ((f | X) . x) in [.M1, M2.] by A62, A55, A75;

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

              then ((f | X) . x) in N3 by A49, A77;

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

            end;

            hence thesis by FCONT_1: 4;

          end;

          hence thesis by FCONT_1:def 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_3:13

    

     Th13: X c= ( dom f) & (f | X) is monotone & (ex p st (f .: X) = ( left_closed_halfline p)) implies (f | X) is continuous

    proof

      assume that

       A1: X c= ( dom f) and

       A2: (f | X) is monotone;

      given p such that

       A3: (f .: X) = ( left_closed_halfline p);

      set L = ( left_open_halfline p);

      set l = ( left_closed_halfline p);

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

      proof

        let x0 be Real;

        

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

        

         A5: L c= l by XXREAL_1: 21;

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

        then x0 in X;

        then x0 in (( dom f) /\ X) by A1, XBOOLE_0:def 4;

        then

         A6: x0 in ( dom (f | X)) by RELAT_1: 61;

        then ((f | X) . x0) in ((f | X) .: X) by FUNCT_1:def 6;

        then ((f | X) . x0) in ( {p} \/ L) by A3, A4, XXREAL_1: 423;

        then

         A7: ((f | X) . x0) in {p} or ((f | X) . x0) in L by XBOOLE_0:def 3;

        now

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

          now

            per cases by A2, RFUNCT_2:def 5;

              suppose (f | X) is non-decreasing;

              then

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

              now

                per cases by A7, TARSKI:def 1;

                  suppose ((f | X) . x0) in L;

                  then

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

                   A9: N2 c= L by RCOMP_1: 18;

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

                   A10: N3 c= N1 and

                   A11: N3 c= N2 by RCOMP_1: 17;

                  consider r be Real such that

                   A12: r > 0 and

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

                  reconsider r as Real;

                  

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

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

                  

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

                  

                   A16: ((f | X) . x0) < (((f | X) . x0) + r) by A12, 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 A15, XXREAL_0: 2;

                  then

                   A17: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A14;

                  then M2 in N2 by A11, A13;

                  then M2 in L by A9;

                  then

                  consider r2 be Element of REAL such that

                   A18: r2 in ( dom (f | X)) & r2 in X and

                   A19: M2 = ((f | X) . r2) by A3, A4, A5, PARTFUN2: 59;

                  

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

                   A21:

                  now

                    assume

                     A22: r2 < x0;

                    x0 in (X /\ ( dom (f | X))) & r2 in (X /\ ( dom (f | X))) by A6, A18, XBOOLE_0:def 4;

                    hence contradiction by A8, A19, A20, A22, RFUNCT_2: 22;

                  end;

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

                  

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

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

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

                  then

                   A24: M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A23;

                  then M1 in N2 by A11, A13;

                  then M1 in L by A9;

                  then

                  consider r1 be Element of REAL such that

                   A25: r1 in ( dom (f | X)) & r1 in X and

                   A26: M1 = ((f | X) . r1) by A3, A4, A5, PARTFUN2: 59;

                  

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

                  then

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

                   A29:

                  now

                    assume

                     A30: x0 < r1;

                    x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A6, A25, XBOOLE_0:def 4;

                    hence contradiction by A8, A26, A28, A30, RFUNCT_2: 22;

                  end;

                  x0 <> r2 by A12, A19, XREAL_1: 29, XREAL_1: 215;

                  then x0 < r2 by A21, XXREAL_0: 1;

                  then

                   A31: (r2 - x0) > 0 by XREAL_1: 50;

                  set R = ( min ((x0 - r1),(r2 - x0)));

                  

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

                  r1 <> x0 by A26, A27, XREAL_1: 19;

                  then r1 < x0 by A29, XXREAL_0: 1;

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

                  then R > 0 by A31, 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

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

                   A34: x in N;

                  

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

                  

                   A36: ex s st s = x & (x0 - R) < s & s < (x0 + R) by A34;

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

                  then

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

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

                  then (x0 - x) < (x0 - r1) by A37, XXREAL_0: 2;

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

                  then

                   A38: ((x - x0) + x0) > ((r1 - x0) + x0) by XREAL_1: 6;

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

                  then

                   A39: ((f | X) . r1) <= ((f | X) . x) by A8, A38, A35, RFUNCT_2: 22;

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

                  then (x - x0) < (r2 - x0) by A32, XXREAL_0: 2;

                  then

                   A40: ((x - x0) + x0) < ((r2 - x0) + x0) by XREAL_1: 6;

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

                  then ((f | X) . x) <= ((f | X) . r2) by A8, A40, A35, RFUNCT_2: 22;

                  then

                   A41: ((f | X) . x) in [.M1, M2.] by A26, A19, A39;

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

                  then ((f | X) . x) in N3 by A13, A41;

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

                end;

                  suppose

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

                  then

                  consider r be Real such that

                   A43: r > 0 and

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

                  reconsider r as Real;

                  set R = (r / 2);

                  

                   A45: p < (p + R) by A43, XREAL_1: 29, XREAL_1: 215;

                  

                   A46: (p - R) < p by A43, XREAL_1: 44, XREAL_1: 215;

                  then (p - R) in { s : s < p };

                  then (p - R) in L by XXREAL_1: 229;

                  then

                  consider r1 be Element of REAL such that

                   A47: r1 in ( dom (f | X)) & r1 in X and

                   A48: (p - R) = ((f | X) . r1) by A3, A4, A5, PARTFUN2: 59;

                  

                   A49: r1 in (X /\ ( dom (f | X))) by A47, XBOOLE_0:def 4;

                   A50:

                  now

                    assume

                     A51: x0 < r1;

                    x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A6, A47, XBOOLE_0:def 4;

                    hence contradiction by A8, A42, A46, A48, A51, RFUNCT_2: 22;

                  end;

                  r1 <> x0 by A42, A43, A48, XREAL_1: 44, XREAL_1: 215;

                  then r1 < x0 by A50, XXREAL_0: 1;

                  then

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

                  take N;

                  let x be Real such that

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

                   A53: x in N;

                  

                   A54: ex s st s = x & (x0 - (x0 - r1)) < s & s < (x0 + (x0 - r1)) by A53;

                  

                   A55: R < r by A43, XREAL_1: 216;

                  then

                   A56: (p - r) < (p - R) by XREAL_1: 15;

                  ((f | X) . x) in l by A3, A4, A52, FUNCT_1:def 6;

                  then ((f | X) . x) in { s : s <= p } by XXREAL_1: 231;

                  then ex s st s = ((f | X) . x) & s <= p;

                  then

                   A57: ((f | X) . x) <= (p + R) by A45, XXREAL_0: 2;

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

                  then (p - R) <= ((f | X) . x) by A8, A48, A49, A54, RFUNCT_2: 22;

                  then

                   A58: ((f | X) . x) in [.(p - R), (p + R).] by A57;

                  p < (p + r) by A43, XREAL_1: 29;

                  then (p - R) < (p + r) by A46, XXREAL_0: 2;

                  then

                   A59: (p - R) in ].(p - r), (p + r).[ by A56;

                  

                   A60: (p + R) < (p + r) by A55, XREAL_1: 6;

                  (p - r) < p by A43, XREAL_1: 44;

                  then (p - r) < (p + R) by A45, XXREAL_0: 2;

                  then (p + R) in ].(p - r), (p + r).[ by A60;

                  then [.(p - R), (p + R).] c= N1 by A44, A59, XXREAL_2:def 12;

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

                end;

              end;

              hence ex N be Neighbourhood of x0 st for r1 be Real st r1 in ( dom (f | X)) & r1 in N holds ((f | X) . r1) in N1;

            end;

              suppose (f | X) is non-increasing;

              then

               A61: ((f | X) | X) is non-increasing;

              now

                per cases by A7, TARSKI:def 1;

                  suppose ((f | X) . x0) in L;

                  then

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

                   A62: N2 c= L by RCOMP_1: 18;

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

                   A63: N3 c= N1 and

                   A64: N3 c= N2 by RCOMP_1: 17;

                  consider r be Real such that

                   A65: r > 0 and

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

                  reconsider r as Real;

                  

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

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

                  

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

                  

                   A69: ((f | X) . x0) < (((f | X) . x0) + r) by A65, 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 A68, XXREAL_0: 2;

                  then

                   A70: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A67;

                  then M2 in N2 by A64, A66;

                  then M2 in L by A62;

                  then

                  consider r2 be Element of REAL such that

                   A71: r2 in ( dom (f | X)) & r2 in X and

                   A72: M2 = ((f | X) . r2) by A3, A4, A5, PARTFUN2: 59;

                  

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

                   A74:

                  now

                    assume

                     A75: r2 > x0;

                    x0 in (X /\ ( dom (f | X))) & r2 in (X /\ ( dom (f | X))) by A6, A71, XBOOLE_0:def 4;

                    hence contradiction by A61, A72, A73, A75, RFUNCT_2: 23;

                  end;

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

                  

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

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

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

                  then

                   A77: M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A76;

                  then M1 in N2 by A64, A66;

                  then M1 in L by A62;

                  then

                  consider r1 be Element of REAL such that

                   A78: r1 in ( dom (f | X)) & r1 in X and

                   A79: M1 = ((f | X) . r1) by A3, A4, A5, PARTFUN2: 59;

                  

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

                  then

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

                   A82:

                  now

                    assume

                     A83: x0 > r1;

                    x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A6, A78, XBOOLE_0:def 4;

                    hence contradiction by A61, A79, A81, A83, RFUNCT_2: 23;

                  end;

                  x0 <> r2 by A65, A72, XREAL_1: 29, XREAL_1: 215;

                  then x0 > r2 by A74, XXREAL_0: 1;

                  then

                   A84: (x0 - r2) > 0 by XREAL_1: 50;

                  set R = ( min ((r1 - x0),(x0 - r2)));

                  

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

                  r1 <> x0 by A79, A80, XREAL_1: 19;

                  then r1 > x0 by A82, XXREAL_0: 1;

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

                  then R > 0 by A84, 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

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

                   A87: x in N;

                  

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

                  

                   A89: ex s st s = x & (x0 - R) < s & s < (x0 + R) by A87;

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

                  then

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

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

                  then (x - x0) < (r1 - x0) by A85, XXREAL_0: 2;

                  then

                   A91: ((x - x0) + x0) < ((r1 - x0) + x0) by XREAL_1: 6;

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

                  then

                   A92: ((f | X) . r1) <= ((f | X) . x) by A61, A91, A88, RFUNCT_2: 23;

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

                  then (x0 - x) < (x0 - r2) by A90, XXREAL_0: 2;

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

                  then

                   A93: ((x - x0) + x0) > ((r2 - x0) + x0) by XREAL_1: 6;

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

                  then ((f | X) . x) <= ((f | X) . r2) by A61, A93, A88, RFUNCT_2: 23;

                  then

                   A94: ((f | X) . x) in [.M1, M2.] by A79, A72, A92;

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

                  then ((f | X) . x) in N3 by A66, A94;

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

                end;

                  suppose

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

                  then

                  consider r be Real such that

                   A96: r > 0 and

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

                  reconsider r as Real;

                  set R = (r / 2);

                  

                   A98: p < (p + R) by A96, XREAL_1: 29, XREAL_1: 215;

                  

                   A99: (p - R) < p by A96, XREAL_1: 44, XREAL_1: 215;

                  then (p - R) in { s : s < p };

                  then (p - R) in L by XXREAL_1: 229;

                  then

                  consider r1 be Element of REAL such that

                   A100: r1 in ( dom (f | X)) & r1 in X and

                   A101: (p - R) = ((f | X) . r1) by A3, A4, A5, PARTFUN2: 59;

                  

                   A102: r1 in (X /\ ( dom (f | X))) by A100, XBOOLE_0:def 4;

                   A103:

                  now

                    assume

                     A104: x0 > r1;

                    x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A6, A100, XBOOLE_0:def 4;

                    hence contradiction by A61, A95, A99, A101, A104, RFUNCT_2: 23;

                  end;

                  r1 <> x0 by A95, A96, A101, XREAL_1: 44, XREAL_1: 215;

                  then r1 > x0 by A103, XXREAL_0: 1;

                  then

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

                  take N;

                  let x be Real such that

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

                   A106: x in N;

                  

                   A107: ex s st s = x & (x0 - (r1 - x0)) < s & s < (x0 + (r1 - x0)) by A106;

                  

                   A108: R < r by A96, XREAL_1: 216;

                  then

                   A109: (p - r) < (p - R) by XREAL_1: 15;

                  ((f | X) . x) in l by A3, A4, A105, FUNCT_1:def 6;

                  then ((f | X) . x) in { s : s <= p } by XXREAL_1: 231;

                  then ex s st s = ((f | X) . x) & s <= p;

                  then

                   A110: ((f | X) . x) <= (p + R) by A98, XXREAL_0: 2;

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

                  then (p - R) <= ((f | X) . x) by A61, A101, A102, A107, RFUNCT_2: 23;

                  then

                   A111: ((f | X) . x) in [.(p - R), (p + R).] by A110;

                  p < (p + r) by A96, XREAL_1: 29;

                  then (p - R) < (p + r) by A99, XXREAL_0: 2;

                  then

                   A112: (p - R) in ].(p - r), (p + r).[ by A109;

                  

                   A113: (p + R) < (p + r) by A108, XREAL_1: 6;

                  (p - r) < p by A96, XREAL_1: 44;

                  then (p - r) < (p + R) by A98, XXREAL_0: 2;

                  then (p + R) in ].(p - r), (p + r).[ by A113;

                  then [.(p - R), (p + R).] c= N1 by A97, A112, XXREAL_2:def 12;

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

                end;

              end;

              hence ex N be Neighbourhood of x0 st for r1 be Real st r1 in ( dom (f | X)) & r1 in N holds ((f | X) . r1) in N1;

            end;

          end;

          hence ex N be Neighbourhood of x0 st for r1 be Real st r1 in ( dom (f | X)) & r1 in N holds ((f | X) . r1) in N1;

        end;

        hence thesis by FCONT_1: 4;

      end;

      hence thesis by FCONT_1:def 2;

    end;

    theorem :: FCONT_3:14

    

     Th14: X c= ( dom f) & (f | X) is monotone & (ex p st (f .: X) = ( right_closed_halfline p)) implies (f | X) is continuous

    proof

      assume that

       A1: X c= ( dom f) and

       A2: (f | X) is monotone;

      given p such that

       A3: (f .: X) = ( right_closed_halfline p);

      set L = ( right_open_halfline p);

      set l = ( right_closed_halfline p);

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

      proof

        let x0 be Real;

        

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

        

         A5: L c= l by XXREAL_1: 22;

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

        then x0 in X;

        then x0 in (( dom f) /\ X) by A1, XBOOLE_0:def 4;

        then

         A6: x0 in ( dom (f | X)) by RELAT_1: 61;

        then ((f | X) . x0) in ((f | X) .: X) by FUNCT_1:def 6;

        then ((f | X) . x0) in ( {p} \/ L) by A3, A4, XXREAL_1: 427;

        then

         A7: ((f | X) . x0) in {p} or ((f | X) . x0) in L by XBOOLE_0:def 3;

        now

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

          now

            per cases by A2, RFUNCT_2:def 5;

              suppose (f | X) is non-decreasing;

              then

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

              now

                per cases by A7, TARSKI:def 1;

                  suppose ((f | X) . x0) in L;

                  then

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

                   A9: N2 c= L by RCOMP_1: 18;

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

                   A10: N3 c= N1 and

                   A11: N3 c= N2 by RCOMP_1: 17;

                  consider r be Real such that

                   A12: r > 0 and

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

                  reconsider r as Real;

                  

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

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

                  

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

                  

                   A16: ((f | X) . x0) < (((f | X) . x0) + r) by A12, 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 A15, XXREAL_0: 2;

                  then

                   A17: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A14;

                  then M2 in N2 by A11, A13;

                  then M2 in L by A9;

                  then

                  consider r2 be Element of REAL such that

                   A18: r2 in ( dom (f | X)) & r2 in X and

                   A19: M2 = ((f | X) . r2) by A3, A4, A5, PARTFUN2: 59;

                  

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

                   A21:

                  now

                    assume

                     A22: r2 < x0;

                    x0 in (X /\ ( dom (f | X))) & r2 in (X /\ ( dom (f | X))) by A6, A18, XBOOLE_0:def 4;

                    hence contradiction by A8, A19, A20, A22, RFUNCT_2: 22;

                  end;

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

                  

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

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

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

                  then

                   A24: M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A23;

                  then M1 in N2 by A11, A13;

                  then M1 in L by A9;

                  then

                  consider r1 be Element of REAL such that

                   A25: r1 in ( dom (f | X)) & r1 in X and

                   A26: M1 = ((f | X) . r1) by A3, A4, A5, PARTFUN2: 59;

                  

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

                  then

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

                   A29:

                  now

                    assume

                     A30: x0 < r1;

                    x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A6, A25, XBOOLE_0:def 4;

                    hence contradiction by A8, A26, A28, A30, RFUNCT_2: 22;

                  end;

                  x0 <> r2 by A12, A19, XREAL_1: 29, XREAL_1: 215;

                  then x0 < r2 by A21, XXREAL_0: 1;

                  then

                   A31: (r2 - x0) > 0 by XREAL_1: 50;

                  set R = ( min ((x0 - r1),(r2 - x0)));

                  

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

                  r1 <> x0 by A26, A27, XREAL_1: 19;

                  then r1 < x0 by A29, XXREAL_0: 1;

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

                  then R > 0 by A31, 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

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

                   A34: x in N;

                  

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

                  

                   A36: ex s st s = x & (x0 - R) < s & s < (x0 + R) by A34;

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

                  then

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

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

                  then (x0 - x) < (x0 - r1) by A37, XXREAL_0: 2;

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

                  then

                   A38: ((x - x0) + x0) > ((r1 - x0) + x0) by XREAL_1: 6;

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

                  then

                   A39: ((f | X) . r1) <= ((f | X) . x) by A8, A38, A35, RFUNCT_2: 22;

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

                  then (x - x0) < (r2 - x0) by A32, XXREAL_0: 2;

                  then

                   A40: ((x - x0) + x0) < ((r2 - x0) + x0) by XREAL_1: 6;

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

                  then ((f | X) . x) <= ((f | X) . r2) by A8, A40, A35, RFUNCT_2: 22;

                  then

                   A41: ((f | X) . x) in [.M1, M2.] by A26, A19, A39;

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

                  then ((f | X) . x) in N3 by A13, A41;

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

                end;

                  suppose

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

                  then

                  consider r be Real such that

                   A43: r > 0 and

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

                  reconsider r as Real;

                  set R = (r / 2);

                  

                   A45: (p - R) < p by A43, XREAL_1: 44, XREAL_1: 215;

                  

                   A46: p < (p + R) by A43, XREAL_1: 29, XREAL_1: 215;

                  then (p + R) in { s : p < s };

                  then (p + R) in L by XXREAL_1: 230;

                  then

                  consider r1 be Element of REAL such that

                   A47: r1 in ( dom (f | X)) & r1 in X and

                   A48: (p + R) = ((f | X) . r1) by A3, A4, A5, PARTFUN2: 59;

                   A49:

                  now

                    assume

                     A50: x0 > r1;

                    x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A6, A47, XBOOLE_0:def 4;

                    hence contradiction by A8, A42, A46, A48, A50, RFUNCT_2: 22;

                  end;

                  r1 <> x0 by A42, A43, A48, XREAL_1: 29, XREAL_1: 215;

                  then r1 > x0 by A49, XXREAL_0: 1;

                  then

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

                  take N;

                  let x be Real such that

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

                   A52: x in N;

                  

                   A53: ex s st s = x & (x0 - (r1 - x0)) < s & s < (x0 + (r1 - x0)) by A52;

                  ((f | X) . x) in l by A3, A4, A51, FUNCT_1:def 6;

                  then ((f | X) . x) in { s : p <= s } by XXREAL_1: 232;

                  then ex s st s = ((f | X) . x) & p <= s;

                  then

                   A54: (p - R) <= ((f | X) . x) by A45, XXREAL_0: 2;

                  

                   A55: r1 in (X /\ ( dom (f | X))) by A47, XBOOLE_0:def 4;

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

                  then (p + R) >= ((f | X) . x) by A8, A48, A55, A53, RFUNCT_2: 22;

                  then

                   A56: ((f | X) . x) in [.(p - R), (p + R).] by A54;

                  

                   A57: R < r by A43, XREAL_1: 216;

                  then

                   A58: (p - r) < (p - R) by XREAL_1: 15;

                  p < (p + r) by A43, XREAL_1: 29;

                  then (p - R) < (p + r) by A45, XXREAL_0: 2;

                  then

                   A59: (p - R) in ].(p - r), (p + r).[ by A58;

                  

                   A60: (p + R) < (p + r) by A57, XREAL_1: 6;

                  (p - r) < p by A43, XREAL_1: 44;

                  then (p - r) < (p + R) by A46, XXREAL_0: 2;

                  then (p + R) in ].(p - r), (p + r).[ by A60;

                  then [.(p - R), (p + R).] c= N1 by A44, A59, XXREAL_2:def 12;

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

                end;

              end;

              hence ex N be Neighbourhood of x0 st for r1 be Real st r1 in ( dom (f | X)) & r1 in N holds ((f | X) . r1) in N1;

            end;

              suppose (f | X) is non-increasing;

              then

               A61: ((f | X) | X) is non-increasing;

              now

                per cases by A7, TARSKI:def 1;

                  suppose ((f | X) . x0) in L;

                  then

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

                   A62: N2 c= L by RCOMP_1: 18;

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

                   A63: N3 c= N1 and

                   A64: N3 c= N2 by RCOMP_1: 17;

                  consider r be Real such that

                   A65: r > 0 and

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

                  reconsider r as Real;

                  

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

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

                  

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

                  

                   A69: ((f | X) . x0) < (((f | X) . x0) + r) by A65, 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 A68, XXREAL_0: 2;

                  then

                   A70: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A67;

                  then M2 in N2 by A64, A66;

                  then M2 in L by A62;

                  then

                  consider r2 be Element of REAL such that

                   A71: r2 in ( dom (f | X)) & r2 in X and

                   A72: M2 = ((f | X) . r2) by A3, A4, A5, PARTFUN2: 59;

                  

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

                   A74:

                  now

                    assume

                     A75: r2 > x0;

                    x0 in (X /\ ( dom (f | X))) & r2 in (X /\ ( dom (f | X))) by A6, A71, XBOOLE_0:def 4;

                    hence contradiction by A61, A72, A73, A75, RFUNCT_2: 23;

                  end;

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

                  

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

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

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

                  then

                   A77: M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A76;

                  then M1 in N2 by A64, A66;

                  then M1 in L by A62;

                  then

                  consider r1 be Element of REAL such that

                   A78: r1 in ( dom (f | X)) & r1 in X and

                   A79: M1 = ((f | X) . r1) by A3, A4, A5, PARTFUN2: 59;

                  

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

                  then

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

                   A82:

                  now

                    assume

                     A83: x0 > r1;

                    x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A6, A78, XBOOLE_0:def 4;

                    hence contradiction by A61, A79, A81, A83, RFUNCT_2: 23;

                  end;

                  x0 <> r2 by A65, A72, XREAL_1: 29, XREAL_1: 215;

                  then x0 > r2 by A74, XXREAL_0: 1;

                  then

                   A84: (x0 - r2) > 0 by XREAL_1: 50;

                  set R = ( min ((r1 - x0),(x0 - r2)));

                  

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

                  r1 <> x0 by A79, A80, XREAL_1: 19;

                  then r1 > x0 by A82, XXREAL_0: 1;

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

                  then R > 0 by A84, 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

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

                   A87: x in N;

                  

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

                  

                   A89: ex s st s = x & (x0 - R) < s & s < (x0 + R) by A87;

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

                  then

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

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

                  then (x - x0) < (r1 - x0) by A85, XXREAL_0: 2;

                  then

                   A91: ((x - x0) + x0) < ((r1 - x0) + x0) by XREAL_1: 6;

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

                  then

                   A92: ((f | X) . r1) <= ((f | X) . x) by A61, A91, A88, RFUNCT_2: 23;

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

                  then (x0 - x) < (x0 - r2) by A90, XXREAL_0: 2;

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

                  then

                   A93: ((x - x0) + x0) > ((r2 - x0) + x0) by XREAL_1: 6;

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

                  then ((f | X) . x) <= ((f | X) . r2) by A61, A93, A88, RFUNCT_2: 23;

                  then

                   A94: ((f | X) . x) in [.M1, M2.] by A79, A72, A92;

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

                  then ((f | X) . x) in N3 by A66, A94;

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

                end;

                  suppose

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

                  then

                  consider r be Real such that

                   A96: r > 0 and

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

                  reconsider r as Real;

                  set R = (r / 2);

                  

                   A98: (p - R) < p by A96, XREAL_1: 44, XREAL_1: 215;

                  

                   A99: p < (p + R) by A96, XREAL_1: 29, XREAL_1: 215;

                  then (p + R) in { s : p < s };

                  then (p + R) in L by XXREAL_1: 230;

                  then

                  consider r1 be Element of REAL such that

                   A100: r1 in ( dom (f | X)) & r1 in X and

                   A101: (p + R) = ((f | X) . r1) by A3, A4, A5, PARTFUN2: 59;

                   A102:

                  now

                    assume

                     A103: x0 < r1;

                    x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A6, A100, XBOOLE_0:def 4;

                    hence contradiction by A61, A95, A99, A101, A103, RFUNCT_2: 23;

                  end;

                  r1 <> x0 by A95, A96, A101, XREAL_1: 29, XREAL_1: 215;

                  then r1 < x0 by A102, XXREAL_0: 1;

                  then

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

                  take N;

                  let x be Real such that

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

                   A105: x in N;

                  

                   A106: ex s st s = x & (x0 - (x0 - r1)) < s & s < (x0 + (x0 - r1)) by A105;

                  ((f | X) . x) in l by A3, A4, A104, FUNCT_1:def 6;

                  then ((f | X) . x) in { s : p <= s } by XXREAL_1: 232;

                  then ex s st s = ((f | X) . x) & p <= s;

                  then

                   A107: (p - R) <= ((f | X) . x) by A98, XXREAL_0: 2;

                  

                   A108: r1 in (X /\ ( dom (f | X))) by A100, XBOOLE_0:def 4;

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

                  then (p + R) >= ((f | X) . x) by A61, A101, A108, A106, RFUNCT_2: 23;

                  then

                   A109: ((f | X) . x) in [.(p - R), (p + R).] by A107;

                  

                   A110: R < r by A96, XREAL_1: 216;

                  then

                   A111: (p - r) < (p - R) by XREAL_1: 15;

                  p < (p + r) by A96, XREAL_1: 29;

                  then (p - R) < (p + r) by A98, XXREAL_0: 2;

                  then

                   A112: (p - R) in ].(p - r), (p + r).[ by A111;

                  

                   A113: (p + R) < (p + r) by A110, XREAL_1: 6;

                  (p - r) < p by A96, XREAL_1: 44;

                  then (p - r) < (p + R) by A99, XXREAL_0: 2;

                  then (p + R) in ].(p - r), (p + r).[ by A113;

                  then [.(p - R), (p + R).] c= N1 by A97, A112, XXREAL_2:def 12;

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

                end;

              end;

              hence ex N be Neighbourhood of x0 st for r1 be Real st r1 in ( dom (f | X)) & r1 in N holds ((f | X) . r1) in N1;

            end;

          end;

          hence ex N be Neighbourhood of x0 st for r1 be Real st r1 in ( dom (f | X)) & r1 in N holds ((f | X) . r1) in N1;

        end;

        hence thesis by FCONT_1: 4;

      end;

      hence thesis by FCONT_1:def 2;

    end;

    theorem :: FCONT_3:15

    

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

    proof

      assume that

       A1: X c= ( dom f) and

       A2: (f | X) is monotone;

      given p, g such that

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

      set L = ].p, g.[;

      now

        per cases by A2, RFUNCT_2:def 5;

          suppose (f | X) is non-decreasing;

          then

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

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

          proof

            let x0 be Real;

            

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

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

            then x0 in X;

            then x0 in (( dom f) /\ X) by A1, XBOOLE_0:def 4;

            then

             A6: x0 in ( dom (f | X)) by RELAT_1: 61;

            then ((f | X) . x0) in ((f | X) .: X) by FUNCT_1:def 6;

            then

             A7: ((f | X) . x0) in L by A3, RELAT_1: 129;

            now

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

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

               A8: N2 c= L by A7, RCOMP_1: 18;

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

               A9: N3 c= N1 and

               A10: N3 c= N2 by RCOMP_1: 17;

              consider r be Real such that

               A11: r > 0 and

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

              reconsider r as Real;

              

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

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

              

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

              

               A15: ((f | X) . x0) < (((f | X) . x0) + r) by A11, 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 A14, XXREAL_0: 2;

              then

               A16: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A13;

              then M2 in N2 by A10, A12;

              then

              consider r2 be Element of REAL such that

               A17: r2 in ( dom (f | X)) & r2 in X and

               A18: M2 = ((f | X) . r2) by A3, A5, A8, PARTFUN2: 59;

              

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

               A20:

              now

                assume

                 A21: r2 < x0;

                x0 in (X /\ ( dom (f | X))) & r2 in (X /\ ( dom (f | X))) by A6, A17, XBOOLE_0:def 4;

                hence contradiction by A4, A18, A19, A21, RFUNCT_2: 22;

              end;

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

              

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

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

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

              then

               A23: M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A22;

              then M1 in N2 by A10, A12;

              then

              consider r1 be Element of REAL such that

               A24: r1 in ( dom (f | X)) & r1 in X and

               A25: M1 = ((f | X) . r1) by A3, A5, A8, PARTFUN2: 59;

              

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

              then

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

               A28:

              now

                assume

                 A29: x0 < r1;

                x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A6, A24, XBOOLE_0:def 4;

                hence contradiction by A4, A25, A27, A29, RFUNCT_2: 22;

              end;

              x0 <> r2 by A11, A18, XREAL_1: 29, XREAL_1: 215;

              then x0 < r2 by A20, XXREAL_0: 1;

              then

               A30: (r2 - x0) > 0 by XREAL_1: 50;

              set R = ( min ((x0 - r1),(r2 - x0)));

              

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

              r1 <> x0 by A25, A26, XREAL_1: 19;

              then r1 < x0 by A28, XXREAL_0: 1;

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

              then R > 0 by A30, 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

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

               A33: x in N;

              

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

              

               A35: ex s st s = x & (x0 - R) < s & s < (x0 + R) by A33;

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

              then

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

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

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

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

              then

               A37: ((x - x0) + x0) > ((r1 - x0) + x0) by XREAL_1: 6;

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

              then

               A38: ((f | X) . r1) <= ((f | X) . x) by A4, A37, A34, RFUNCT_2: 22;

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

              then (x - x0) < (r2 - x0) by A31, XXREAL_0: 2;

              then

               A39: ((x - x0) + x0) < ((r2 - x0) + x0) by XREAL_1: 6;

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

              then ((f | X) . x) <= ((f | X) . r2) by A4, A39, A34, RFUNCT_2: 22;

              then

               A40: ((f | X) . x) in [.M1, M2.] by A25, A18, A38;

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

              then ((f | X) . x) in N3 by A12, A40;

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

            end;

            hence thesis by FCONT_1: 4;

          end;

          hence thesis by FCONT_1:def 2;

        end;

          suppose (f | X) is non-increasing;

          then

           A41: ((f | X) | X) is non-increasing;

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

          proof

            let x0 be Real;

            

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

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

            then x0 in X;

            then x0 in (( dom f) /\ X) by A1, XBOOLE_0:def 4;

            then

             A43: x0 in ( dom (f | X)) by RELAT_1: 61;

            then ((f | X) . x0) in ((f | X) .: X) by FUNCT_1:def 6;

            then

             A44: ((f | X) . x0) in L by A3, RELAT_1: 129;

            now

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

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

               A45: N2 c= L by A44, RCOMP_1: 18;

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

               A46: N3 c= N1 and

               A47: N3 c= N2 by RCOMP_1: 17;

              consider r be Real such that

               A48: r > 0 and

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

              reconsider r as Real;

              

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

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

              

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

              

               A52: ((f | X) . x0) < (((f | X) . x0) + r) by A48, 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 A51, XXREAL_0: 2;

              then

               A53: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A50;

              then M2 in N2 by A47, A49;

              then

              consider r2 be Element of REAL such that

               A54: r2 in ( dom (f | X)) & r2 in X and

               A55: M2 = ((f | X) . r2) by A3, A42, A45, PARTFUN2: 59;

              

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

               A57:

              now

                assume

                 A58: r2 > x0;

                x0 in (X /\ ( dom (f | X))) & r2 in (X /\ ( dom (f | X))) by A43, A54, XBOOLE_0:def 4;

                hence contradiction by A41, A55, A56, A58, RFUNCT_2: 23;

              end;

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

              

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

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

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

              then

               A60: M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A59;

              then M1 in N2 by A47, A49;

              then

              consider r1 be Element of REAL such that

               A61: r1 in ( dom (f | X)) & r1 in X and

               A62: M1 = ((f | X) . r1) by A3, A42, A45, PARTFUN2: 59;

              

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

              then

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

               A65:

              now

                assume

                 A66: x0 > r1;

                x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A43, A61, XBOOLE_0:def 4;

                hence contradiction by A41, A62, A64, A66, RFUNCT_2: 23;

              end;

              x0 <> r2 by A48, A55, XREAL_1: 29, XREAL_1: 215;

              then x0 > r2 by A57, XXREAL_0: 1;

              then

               A67: (x0 - r2) > 0 by XREAL_1: 50;

              set R = ( min ((r1 - x0),(x0 - r2)));

              

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

              r1 <> x0 by A62, A63, XREAL_1: 19;

              then r1 > x0 by A65, XXREAL_0: 1;

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

              then R > 0 by A67, 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

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

               A70: x in N;

              

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

              

               A72: ex s st s = x & (x0 - R) < s & s < (x0 + R) by A70;

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

              then

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

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

              then (x - x0) < (r1 - x0) by A68, XXREAL_0: 2;

              then

               A74: ((x - x0) + x0) < ((r1 - x0) + x0) by XREAL_1: 6;

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

              then

               A75: ((f | X) . r1) <= ((f | X) . x) by A41, A74, A71, RFUNCT_2: 23;

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

              then (x0 - x) < (x0 - r2) by A73, XXREAL_0: 2;

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

              then

               A76: ((x - x0) + x0) > ((r2 - x0) + x0) by XREAL_1: 6;

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

              then ((f | X) . x) <= ((f | X) . r2) by A41, A76, A71, RFUNCT_2: 23;

              then

               A77: ((f | X) . x) in [.M1, M2.] by A62, A55, A75;

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

              then ((f | X) . x) in N3 by A49, A77;

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

            end;

            hence thesis by FCONT_1: 4;

          end;

          hence thesis by FCONT_1:def 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_3:16

    

     Th16: X c= ( dom f) & (f | X) is monotone & (f .: X) = REAL implies (f | X) is continuous

    proof

      assume that

       A1: X c= ( dom f) and

       A2: (f | X) is monotone and

       A3: (f .: X) = REAL ;

      now

        per cases by A2, RFUNCT_2:def 5;

          suppose (f | X) is non-decreasing;

          then

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

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

          proof

            let x0 be Real;

            

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

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

            then x0 in X;

            then x0 in (( dom f) /\ X) by A1, XBOOLE_0:def 4;

            then

             A6: x0 in ( dom (f | X)) by RELAT_1: 61;

            now

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

              consider r be Real such that

               A7: r > 0 and

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

              reconsider r as Real;

              

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

              reconsider M1 = (((f | X) . x0) - (r / 2)) as Element of REAL by XREAL_0:def 1;

              consider r1 be Element of REAL such that

               A10: r1 in ( dom (f | X)) & r1 in X and

               A11: M1 = ((f | X) . r1) by A3, A5, PARTFUN2: 59;

              

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

              then

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

               A14:

              now

                assume

                 A15: x0 < r1;

                x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A6, A10, XBOOLE_0:def 4;

                hence contradiction by A4, A11, A13, A15, RFUNCT_2: 22;

              end;

              reconsider M2 = (((f | X) . x0) + (r / 2)) as Element of REAL by XREAL_0:def 1;

              consider r2 be Element of REAL such that

               A16: r2 in ( dom (f | X)) & r2 in X and

               A17: M2 = ((f | X) . r2) by A3, A5, PARTFUN2: 59;

              

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

               A19:

              now

                assume

                 A20: r2 < x0;

                x0 in (X /\ ( dom (f | X))) & r2 in (X /\ ( dom (f | X))) by A6, A16, XBOOLE_0:def 4;

                hence contradiction by A4, A17, A18, A20, RFUNCT_2: 22;

              end;

              x0 <> r2 by A7, A17, XREAL_1: 29, XREAL_1: 215;

              then x0 < r2 by A19, XXREAL_0: 1;

              then

               A21: (r2 - x0) > 0 by XREAL_1: 50;

              set R = ( min ((x0 - r1),(r2 - x0)));

              

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

              r1 <> x0 by A11, A12, XREAL_1: 19;

              then r1 < x0 by A14, XXREAL_0: 1;

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

              then R > 0 by A21, 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

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

               A24: x in N;

              

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

              

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

              

               A27: ((f | X) . x0) < (((f | X) . x0) + r) by A7, 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 A9, XXREAL_0: 2;

              then

               A28: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A26;

              

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

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

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

              then M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A29;

              then

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

              

               A31: ex s st s = x & (x0 - R) < s & s < (x0 + R) by A24;

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

              then

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

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

              then (x0 - x) < (x0 - r1) by A32, XXREAL_0: 2;

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

              then

               A33: ((x - x0) + x0) > ((r1 - x0) + x0) by XREAL_1: 6;

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

              then

               A34: ((f | X) . r1) <= ((f | X) . x) by A4, A33, A25, RFUNCT_2: 22;

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

              then (x - x0) < (r2 - x0) by A22, XXREAL_0: 2;

              then

               A35: ((x - x0) + x0) < ((r2 - x0) + x0) by XREAL_1: 6;

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

              then ((f | X) . x) <= ((f | X) . r2) by A4, A35, A25, RFUNCT_2: 22;

              then ((f | X) . x) in [.M1, M2.] by A11, A17, A34;

              hence ((f | X) . x) in N1 by A8, A30;

            end;

            hence thesis by FCONT_1: 4;

          end;

          hence thesis by FCONT_1:def 2;

        end;

          suppose (f | X) is non-increasing;

          then

           A36: ((f | X) | X) is non-increasing;

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

          proof

            let x0 be Real;

            

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

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

            then x0 in X;

            then x0 in (( dom f) /\ X) by A1, XBOOLE_0:def 4;

            then

             A38: x0 in ( dom (f | X)) by RELAT_1: 61;

            now

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

              consider r be Real such that

               A39: r > 0 and

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

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

              

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

              reconsider M1 = (((f | X) . x0) - (r / 2)) as Element of REAL by XREAL_0:def 1;

              consider r1 be Element of REAL such that

               A42: r1 in ( dom (f | X)) & r1 in X and

               A43: M1 = ((f | X) . r1) by A3, A37, PARTFUN2: 59;

              

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

              then

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

               A46:

              now

                assume

                 A47: x0 > r1;

                x0 in (X /\ ( dom (f | X))) & r1 in (X /\ ( dom (f | X))) by A38, A42, XBOOLE_0:def 4;

                hence contradiction by A36, A43, A45, A47, RFUNCT_2: 23;

              end;

              reconsider M2 = (((f | X) . x0) + (r / 2)) as Element of REAL by XREAL_0:def 1;

              consider r2 be Element of REAL such that

               A48: r2 in ( dom (f | X)) & r2 in X and

               A49: M2 = ((f | X) . r2) by A3, A37, PARTFUN2: 59;

              

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

               A51:

              now

                assume

                 A52: r2 > x0;

                x0 in (X /\ ( dom (f | X))) & r2 in (X /\ ( dom (f | X))) by A38, A48, XBOOLE_0:def 4;

                hence contradiction by A36, A49, A50, A52, RFUNCT_2: 23;

              end;

              x0 <> r2 by A39, A49, XREAL_1: 29, XREAL_1: 215;

              then x0 > r2 by A51, XXREAL_0: 1;

              then

               A53: (x0 - r2) > 0 by XREAL_1: 50;

              set R = ( min ((r1 - x0),(x0 - r2)));

              

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

              r1 <> x0 by A43, A44, XREAL_1: 19;

              then r1 > x0 by A46, XXREAL_0: 1;

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

              then R > 0 by A53, 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

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

               A56: x in N;

              

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

              

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

              

               A59: ((f | X) . x0) < (((f | X) . x0) + r) by A39, 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 A41, XXREAL_0: 2;

              then

               A60: M2 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A58;

              

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

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

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

              then M1 in ].(((f | X) . x0) - r), (((f | X) . x0) + r).[ by A61;

              then

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

              

               A63: ex s st s = x & (x0 - R) < s & s < (x0 + R) by A56;

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

              then

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

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

              then (x - x0) < (r1 - x0) by A54, XXREAL_0: 2;

              then

               A65: ((x - x0) + x0) < ((r1 - x0) + x0) by XREAL_1: 6;

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

              then

               A66: ((f | X) . r1) <= ((f | X) . x) by A36, A65, A57, RFUNCT_2: 23;

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

              then (x0 - x) < (x0 - r2) by A64, XXREAL_0: 2;

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

              then

               A67: ((x - x0) + x0) > ((r2 - x0) + x0) by XREAL_1: 6;

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

              then ((f | X) . x) <= ((f | X) . r2) by A36, A67, A57, RFUNCT_2: 23;

              then ((f | X) . x) in [.M1, M2.] by A43, A49, A66;

              hence ((f | X) . x) in N1 by A40, A62;

            end;

            hence thesis by FCONT_1: 4;

          end;

          hence thesis by FCONT_1:def 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_3:17

    for f be one-to-one PartFunc of REAL , REAL st ((f | ].p, g.[) is increasing or (f | ].p, g.[) is decreasing) & ].p, g.[ c= ( dom f) holds (((f | ].p, g.[) " ) | (f .: ].p, g.[)) is continuous

    proof

      let f be one-to-one PartFunc of REAL , REAL ;

      assume that

       A1: (f | ].p, g.[) is increasing or (f | ].p, g.[) is decreasing and

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

      now

        per cases by A1;

          suppose

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

           A4:

          now

            let r be Element of REAL ;

            assume r in (f .: ].p, g.[);

            then

            consider s be Element of REAL such that

             A5: s in ( dom f) & s in ].p, g.[ and

             A6: r = (f . s) by PARTFUN2: 59;

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

            then

             A7: s in ( dom (f | ].p, g.[)) by RELAT_1: 61;

            then r = ((f | ].p, g.[) . s) by A6, FUNCT_1: 47;

            then r in ( rng (f | ].p, g.[)) by A7, FUNCT_1:def 3;

            hence r in ( dom ((f | ].p, g.[) " )) by FUNCT_1: 33;

          end;

          

           A8: (((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 A3, Th9;

          hence thesis by A4, A8, Th15, SUBSET_1: 2;

        end;

          suppose

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

           A10:

          now

            let r be Element of REAL ;

            assume r in (f .: ].p, g.[);

            then

            consider s be Element of REAL such that

             A11: s in ( dom f) & s in ].p, g.[ and

             A12: r = (f . s) by PARTFUN2: 59;

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

            then

             A13: s in ( dom (f | ].p, g.[)) by RELAT_1: 61;

            then r = ((f | ].p, g.[) . s) by A12, FUNCT_1: 47;

            then r in ( rng (f | ].p, g.[)) by A13, FUNCT_1:def 3;

            hence r in ( dom ((f | ].p, g.[) " )) by FUNCT_1: 33;

          end;

          

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

          hence thesis by A10, A14, Th15, SUBSET_1: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_3:18

    for f be one-to-one PartFunc of REAL , REAL st ((f | ( left_open_halfline p)) is increasing or (f | ( left_open_halfline p)) is decreasing) & ( left_open_halfline p) c= ( dom f) holds (((f | ( left_open_halfline p)) " ) | (f .: ( left_open_halfline p))) is continuous

    proof

      let f be one-to-one PartFunc of REAL , REAL ;

      set L = ( left_open_halfline p);

      assume that

       A1: (f | L) is increasing or (f | L) is decreasing and

       A2: L c= ( dom f);

      now

        per cases by A1;

          suppose

           A3: (f | L) is increasing;

           A4:

          now

            let r be Element of REAL ;

            assume r in (f .: L);

            then

            consider s be Element of REAL such that

             A5: s in ( dom f) & s in L and

             A6: r = (f . s) by PARTFUN2: 59;

            s in (( dom f) /\ L) by A5, XBOOLE_0:def 4;

            then

             A7: s in ( dom (f | L)) by RELAT_1: 61;

            then r = ((f | L) . s) by A6, FUNCT_1: 47;

            then r in ( rng (f | L)) by A7, FUNCT_1:def 3;

            hence r in ( dom ((f | L) " )) by FUNCT_1: 33;

          end;

          

           A8: (((f | L) " ) .: (f .: L)) = (((f | L) " ) .: ( rng (f | L))) by RELAT_1: 115

          .= (((f | L) " ) .: ( dom ((f | L) " ))) by FUNCT_1: 33

          .= ( rng ((f | L) " )) by RELAT_1: 113

          .= ( dom (f | L)) by FUNCT_1: 33

          .= (( dom f) /\ L) by RELAT_1: 61

          .= L by A2, XBOOLE_1: 28;

          (((f | L) " ) | (f .: L)) is increasing by A3, Th9;

          hence thesis by A4, A8, Th11, SUBSET_1: 2;

        end;

          suppose

           A9: (f | L) is decreasing;

           A10:

          now

            let r be Element of REAL ;

            assume r in (f .: L);

            then

            consider s be Element of REAL such that

             A11: s in ( dom f) & s in L and

             A12: r = (f . s) by PARTFUN2: 59;

            s in (( dom f) /\ L) by A11, XBOOLE_0:def 4;

            then

             A13: s in ( dom (f | L)) by RELAT_1: 61;

            then r = ((f | L) . s) by A12, FUNCT_1: 47;

            then r in ( rng (f | L)) by A13, FUNCT_1:def 3;

            hence r in ( dom ((f | L) " )) by FUNCT_1: 33;

          end;

          

           A14: (((f | L) " ) .: (f .: L)) = (((f | L) " ) .: ( rng (f | L))) by RELAT_1: 115

          .= (((f | L) " ) .: ( dom ((f | L) " ))) by FUNCT_1: 33

          .= ( rng ((f | L) " )) by RELAT_1: 113

          .= ( dom (f | L)) by FUNCT_1: 33

          .= (( dom f) /\ L) by RELAT_1: 61

          .= L by A2, XBOOLE_1: 28;

          (((f | L) " ) | (f .: L)) is decreasing by A9, Th10;

          hence thesis by A10, A14, Th11, SUBSET_1: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_3:19

    for f be one-to-one PartFunc of REAL , REAL st ((f | ( right_open_halfline p)) is increasing or (f | ( right_open_halfline p)) is decreasing) & ( right_open_halfline p) c= ( dom f) holds (((f | ( right_open_halfline p)) " ) | (f .: ( right_open_halfline p))) is continuous

    proof

      let f be one-to-one PartFunc of REAL , REAL ;

      set L = ( right_open_halfline p);

      assume that

       A1: (f | L) is increasing or (f | L) is decreasing and

       A2: L c= ( dom f);

      now

        per cases by A1;

          suppose

           A3: (f | L) is increasing;

           A4:

          now

            let r be Element of REAL ;

            assume r in (f .: L);

            then

            consider s be Element of REAL such that

             A5: s in ( dom f) & s in L and

             A6: r = (f . s) by PARTFUN2: 59;

            s in (( dom f) /\ L) by A5, XBOOLE_0:def 4;

            then

             A7: s in ( dom (f | L)) by RELAT_1: 61;

            then r = ((f | L) . s) by A6, FUNCT_1: 47;

            then r in ( rng (f | L)) by A7, FUNCT_1:def 3;

            hence r in ( dom ((f | L) " )) by FUNCT_1: 33;

          end;

          

           A8: (((f | L) " ) .: (f .: L)) = (((f | L) " ) .: ( rng (f | L))) by RELAT_1: 115

          .= (((f | L) " ) .: ( dom ((f | L) " ))) by FUNCT_1: 33

          .= ( rng ((f | L) " )) by RELAT_1: 113

          .= ( dom (f | L)) by FUNCT_1: 33

          .= (( dom f) /\ L) by RELAT_1: 61

          .= L by A2, XBOOLE_1: 28;

          (((f | L) " ) | (f .: L)) is increasing by A3, Th9;

          hence thesis by A4, A8, Th12, SUBSET_1: 2;

        end;

          suppose

           A9: (f | L) is decreasing;

           A10:

          now

            let r be Element of REAL ;

            assume r in (f .: L);

            then

            consider s be Element of REAL such that

             A11: s in ( dom f) & s in L and

             A12: r = (f . s) by PARTFUN2: 59;

            s in (( dom f) /\ L) by A11, XBOOLE_0:def 4;

            then

             A13: s in ( dom (f | L)) by RELAT_1: 61;

            then r = ((f | L) . s) by A12, FUNCT_1: 47;

            then r in ( rng (f | L)) by A13, FUNCT_1:def 3;

            hence r in ( dom ((f | L) " )) by FUNCT_1: 33;

          end;

          

           A14: (((f | L) " ) .: (f .: L)) = (((f | L) " ) .: ( rng (f | L))) by RELAT_1: 115

          .= (((f | L) " ) .: ( dom ((f | L) " ))) by FUNCT_1: 33

          .= ( rng ((f | L) " )) by RELAT_1: 113

          .= ( dom (f | L)) by FUNCT_1: 33

          .= (( dom f) /\ L) by RELAT_1: 61

          .= L by A2, XBOOLE_1: 28;

          (((f | L) " ) | (f .: L)) is decreasing by A9, Th10;

          hence thesis by A10, A14, Th12, SUBSET_1: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_3:20

    for f be one-to-one PartFunc of REAL , REAL st ((f | ( left_closed_halfline p)) is increasing or (f | ( left_closed_halfline p)) is decreasing) & ( left_closed_halfline p) c= ( dom f) holds (((f | ( left_closed_halfline p)) " ) | (f .: ( left_closed_halfline p))) is continuous

    proof

      let f be one-to-one PartFunc of REAL , REAL ;

      set L = ( left_closed_halfline p);

      assume that

       A1: (f | L) is increasing or (f | L) is decreasing and

       A2: L c= ( dom f);

      now

        per cases by A1;

          suppose

           A3: (f | L) is increasing;

           A4:

          now

            let r be Element of REAL ;

            assume r in (f .: L);

            then

            consider s be Element of REAL such that

             A5: s in ( dom f) & s in L and

             A6: r = (f . s) by PARTFUN2: 59;

            s in (( dom f) /\ L) by A5, XBOOLE_0:def 4;

            then

             A7: s in ( dom (f | L)) by RELAT_1: 61;

            then r = ((f | L) . s) by A6, FUNCT_1: 47;

            then r in ( rng (f | L)) by A7, FUNCT_1:def 3;

            hence r in ( dom ((f | L) " )) by FUNCT_1: 33;

          end;

          

           A8: (((f | L) " ) .: (f .: L)) = (((f | L) " ) .: ( rng (f | L))) by RELAT_1: 115

          .= (((f | L) " ) .: ( dom ((f | L) " ))) by FUNCT_1: 33

          .= ( rng ((f | L) " )) by RELAT_1: 113

          .= ( dom (f | L)) by FUNCT_1: 33

          .= (( dom f) /\ L) by RELAT_1: 61

          .= L by A2, XBOOLE_1: 28;

          (((f | L) " ) | (f .: L)) is increasing by A3, Th9;

          hence thesis by A4, A8, Th13, SUBSET_1: 2;

        end;

          suppose

           A9: (f | L) is decreasing;

           A10:

          now

            let r be Element of REAL ;

            assume r in (f .: L);

            then

            consider s be Element of REAL such that

             A11: s in ( dom f) & s in L and

             A12: r = (f . s) by PARTFUN2: 59;

            s in (( dom f) /\ L) by A11, XBOOLE_0:def 4;

            then

             A13: s in ( dom (f | L)) by RELAT_1: 61;

            then r = ((f | L) . s) by A12, FUNCT_1: 47;

            then r in ( rng (f | L)) by A13, FUNCT_1:def 3;

            hence r in ( dom ((f | L) " )) by FUNCT_1: 33;

          end;

          

           A14: (((f | L) " ) .: (f .: L)) = (((f | L) " ) .: ( rng (f | L))) by RELAT_1: 115

          .= (((f | L) " ) .: ( dom ((f | L) " ))) by FUNCT_1: 33

          .= ( rng ((f | L) " )) by RELAT_1: 113

          .= ( dom (f | L)) by FUNCT_1: 33

          .= (( dom f) /\ L) by RELAT_1: 61

          .= L by A2, XBOOLE_1: 28;

          (((f | L) " ) | (f .: L)) is decreasing by A9, Th10;

          hence thesis by A10, A14, Th13, SUBSET_1: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_3:21

    for f be one-to-one PartFunc of REAL , REAL st ((f | ( right_closed_halfline p)) is increasing or (f | ( right_closed_halfline p)) is decreasing) & ( right_closed_halfline p) c= ( dom f) holds (((f | ( right_closed_halfline p)) " ) | (f .: ( right_closed_halfline p))) is continuous

    proof

      let f be one-to-one PartFunc of REAL , REAL ;

      set L = ( right_closed_halfline p);

      assume that

       A1: (f | L) is increasing or (f | L) is decreasing and

       A2: L c= ( dom f);

      now

        per cases by A1;

          suppose

           A3: (f | L) is increasing;

           A4:

          now

            let r be Element of REAL ;

            assume r in (f .: L);

            then

            consider s be Element of REAL such that

             A5: s in ( dom f) & s in L and

             A6: r = (f . s) by PARTFUN2: 59;

            s in (( dom f) /\ L) by A5, XBOOLE_0:def 4;

            then

             A7: s in ( dom (f | L)) by RELAT_1: 61;

            then r = ((f | L) . s) by A6, FUNCT_1: 47;

            then r in ( rng (f | L)) by A7, FUNCT_1:def 3;

            hence r in ( dom ((f | L) " )) by FUNCT_1: 33;

          end;

          

           A8: (((f | L) " ) .: (f .: L)) = (((f | L) " ) .: ( rng (f | L))) by RELAT_1: 115

          .= (((f | L) " ) .: ( dom ((f | L) " ))) by FUNCT_1: 33

          .= ( rng ((f | L) " )) by RELAT_1: 113

          .= ( dom (f | L)) by FUNCT_1: 33

          .= (( dom f) /\ L) by RELAT_1: 61

          .= L by A2, XBOOLE_1: 28;

          (((f | L) " ) | (f .: L)) is increasing by A3, Th9;

          hence thesis by A4, A8, Th14, SUBSET_1: 2;

        end;

          suppose

           A9: (f | L) is decreasing;

           A10:

          now

            let r be Element of REAL ;

            assume r in (f .: L);

            then

            consider s be Element of REAL such that

             A11: s in ( dom f) & s in L and

             A12: r = (f . s) by PARTFUN2: 59;

            s in (( dom f) /\ L) by A11, XBOOLE_0:def 4;

            then

             A13: s in ( dom (f | L)) by RELAT_1: 61;

            then r = ((f | L) . s) by A12, FUNCT_1: 47;

            then r in ( rng (f | L)) by A13, FUNCT_1:def 3;

            hence r in ( dom ((f | L) " )) by FUNCT_1: 33;

          end;

          

           A14: (((f | L) " ) .: (f .: L)) = (((f | L) " ) .: ( rng (f | L))) by RELAT_1: 115

          .= (((f | L) " ) .: ( dom ((f | L) " ))) by FUNCT_1: 33

          .= ( rng ((f | L) " )) by RELAT_1: 113

          .= ( dom (f | L)) by FUNCT_1: 33

          .= (( dom f) /\ L) by RELAT_1: 61

          .= L by A2, XBOOLE_1: 28;

          (((f | L) " ) | (f .: L)) is decreasing by A9, Th10;

          hence thesis by A10, A14, Th14, SUBSET_1: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_3:22

    for f be one-to-one PartFunc of REAL , REAL st ((f | ( [#] REAL )) is increasing or (f | ( [#] REAL )) is decreasing) & f is total holds ((f " ) | ( rng f)) is continuous

    proof

      set L = ( [#] REAL );

      let f be one-to-one PartFunc of REAL , REAL ;

      assume that

       A1: (f | ( [#] REAL )) is increasing or (f | ( [#] REAL )) is decreasing and

       A2: f is total;

      

       A3: ( dom f) = ( [#] REAL ) by A2, PARTFUN1:def 2;

      now

        per cases by A1;

          suppose

           A4: (f | L) is increasing;

           A5:

          now

            let r be Element of REAL ;

            assume r in (f .: L);

            then

            consider s be Element of REAL such that

             A6: s in ( dom f) and s in L and

             A7: r = (f . s) by PARTFUN2: 59;

            s in (( dom f) /\ L) by A6, XBOOLE_0:def 4;

            then

             A8: s in ( dom (f | L)) by RELAT_1: 61;

            r = ((f | L) . s) by A7;

            then r in ( rng (f | L)) by A8, FUNCT_1:def 3;

            hence r in ( dom ((f | L) " )) by FUNCT_1: 33;

          end;

          

           A9: (((f | L) " ) .: (f .: L)) = (((f | L) " ) .: ( rng (f | L))) by RELAT_1: 115

          .= (((f | L) " ) .: ( dom ((f | L) " ))) by FUNCT_1: 33

          .= ( rng ((f | L) " )) by RELAT_1: 113

          .= ( dom (f | L)) by FUNCT_1: 33

          .= (( dom f) /\ L) by RELAT_1: 61

          .= REAL by A3;

          (((f | L) " ) | (f .: L)) is increasing by A4, Th9;

          then (((f | L) " ) | (f .: L)) is continuous by A5, A9, Th16, SUBSET_1: 2;

          then (((f | L) " ) | ( rng f)) is continuous by A3, RELAT_1: 113;

          hence thesis;

        end;

          suppose

           A10: (f | L) is decreasing;

           A11:

          now

            let r be Element of REAL ;

            assume r in (f .: L);

            then

            consider s be Element of REAL such that

             A12: s in ( dom f) and s in L and

             A13: r = (f . s) by PARTFUN2: 59;

            s in (( dom f) /\ L) by A12, XBOOLE_0:def 4;

            then

             A14: s in ( dom (f | L)) by RELAT_1: 61;

            r = ((f | L) . s) by A13;

            then r in ( rng (f | L)) by A14, FUNCT_1:def 3;

            hence r in ( dom ((f | L) " )) by FUNCT_1: 33;

          end;

          

           A15: (((f | L) " ) .: (f .: L)) = (((f | L) " ) .: ( rng (f | L))) by RELAT_1: 115

          .= (((f | L) " ) .: ( dom ((f | L) " ))) by FUNCT_1: 33

          .= ( rng ((f | L) " )) by RELAT_1: 113

          .= ( dom (f | L)) by FUNCT_1: 33

          .= (( dom f) /\ L) by RELAT_1: 61

          .= REAL by A3;

          (((f | L) " ) | (f .: L)) is decreasing by A10, Th10;

          then (((f | L) " ) | (f .: L)) is continuous by A11, A15, Th16, SUBSET_1: 2;

          then (((f | L) " ) | ( rng f)) is continuous by A3, RELAT_1: 113;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: FCONT_3:23

     ].p, g.[ c= ( dom f) & (f | ].p, g.[) is continuous & ((f | ].p, g.[) is increasing or (f | ].p, g.[) is decreasing) implies ( rng (f | ].p, g.[)) is open

    proof

      assume that

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

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

       A3: (f | ].p, g.[) is increasing or (f | ].p, g.[) is decreasing;

      now

        let r1 be Element of REAL ;

        set f1 = (f | ].p, g.[);

        assume r1 in ( rng f1);

        then

        consider x0 be Element of REAL such that

         A4: x0 in ( dom f1) and

         A5: (f1 . x0) = r1 by PARTFUN1: 3;

        

         A6: r1 = (f . x0) by A4, A5, FUNCT_1: 47;

        

         A7: x0 in (( dom f) /\ ].p, g.[) by A4, RELAT_1: 61;

        then x0 in ].p, g.[ by XBOOLE_0:def 4;

        then

        consider N be Neighbourhood of x0 such that

         A8: N c= ].p, g.[ by RCOMP_1: 18;

        consider r be Real such that

         A9: 0 < r and

         A10: N = ].(x0 - r), (x0 + r).[ by RCOMP_1:def 6;

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

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

        then

         A11: (x0 - (r / 2)) < (x0 - 0 ) by XREAL_1: 15;

        

         A12: (r / 2) < r by A9, XREAL_1: 216;

        then

         A13: (x0 - r) < (x0 - (r / 2)) by XREAL_1: 15;

        

         A14: N c= ( dom f) by A1, A8;

        set fp = (f . (x0 + (r / 2)));

        set fm = (f . (x0 - (r / 2)));

        

         A15: (x0 + (r / 2)) < (x0 + r) by A12, XREAL_1: 8;

        

         A16: x0 < (x0 + (r / 2)) by A9, XREAL_1: 29, XREAL_1: 215;

        then

         A17: (x0 - (r / 2)) < (x0 + (r / 2)) by A11, XXREAL_0: 2;

        x0 < (x0 + r) by A9, XREAL_1: 29;

        then (x0 - (r / 2)) < (x0 + r) by A11, XXREAL_0: 2;

        then

         A18: (x0 - (r / 2)) in ].(x0 - r), (x0 + r).[ by A13;

        then

         A19: (x0 - (r / 2)) in ( ].p, g.[ /\ ( dom f)) by A8, A10, A14, XBOOLE_0:def 4;

        (x0 - r) < x0 by A9, XREAL_1: 44;

        then (x0 - r) < (x0 + (r / 2)) by A16, XXREAL_0: 2;

        then

         A20: (x0 + (r / 2)) in ].(x0 - r), (x0 + r).[ by A15;

        then

         A21: (x0 + (r / 2)) in ( ].p, g.[ /\ ( dom f)) by A8, A10, A14, XBOOLE_0:def 4;

        

         A22: [.(x0 - (r / 2)), (x0 + (r / 2)).] c= ].(x0 - r), (x0 + r).[ by A18, A20, XXREAL_2:def 12;

        

         A23: [.(x0 - (r / 2)), (x0 + (r / 2)).] c= ].p, g.[ by A8, A10, A18, A20, XXREAL_2:def 12;

        then

         A24: (f | [.(x0 - (r / 2)), (x0 + (r / 2)).]) is continuous by A2, FCONT_1: 16;

        now

          per cases by A3;

            suppose

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

            set R = ( min (((f . x0) - fm),(fp - (f . x0))));

            (f . x0) < fp by A7, A16, A21, A25, RFUNCT_2: 20;

            then

             A26: 0 < (fp - (f . x0)) by XREAL_1: 50;

            fm < (f . x0) by A7, A11, A19, A25, RFUNCT_2: 20;

            then 0 < ((f . x0) - fm) by XREAL_1: 50;

            then 0 < R by A26, XXREAL_0: 15;

            then

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

            take N1;

            fm < fp by A17, A21, A19, A25, RFUNCT_2: 20;

            then [.fp, fm.] = {} by XXREAL_1: 29;

            then

             A27: ( [.fm, fp.] \/ [.fp, fm.]) = [.fm, fp.];

            thus N1 c= ( rng f1)

            proof

              let x be object;

              

               A28: ].fm, fp.[ c= [.fm, fp.] by XXREAL_1: 25;

              assume x in N1;

              then

              consider r2 such that

               A29: r2 = x and

               A30: ((f . x0) - R) < r2 and

               A31: r2 < ((f . x0) + R) by A6;

              R <= (fp - (f . x0)) by XXREAL_0: 17;

              then ((f . x0) + R) <= ((f . x0) + (fp - (f . x0))) by XREAL_1: 7;

              then

               A32: r2 < fp by A31, XXREAL_0: 2;

              R <= ((f . x0) - fm) by XXREAL_0: 17;

              then ((f . x0) - ((f . x0) - fm)) <= ((f . x0) - R) by XREAL_1: 13;

              then fm < r2 by A30, XXREAL_0: 2;

              then r2 in ].fm, fp.[ by A32;

              then

              consider s such that

               A33: s in [.(x0 - (r / 2)), (x0 + (r / 2)).] and

               A34: x = (f . s) by A1, A23, A24, A17, A27, A29, A28, FCONT_2: 15, XBOOLE_1: 1;

              s in N by A10, A22, A33;

              then s in (( dom f) /\ ].p, g.[) by A8, A14, XBOOLE_0:def 4;

              then

               A35: s in ( dom f1) by RELAT_1: 61;

              then x = (f1 . s) by A34, FUNCT_1: 47;

              hence thesis by A35, FUNCT_1:def 3;

            end;

          end;

            suppose

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

            set R = ( min ((fm - (f . x0)),((f . x0) - fp)));

            fp < (f . x0) by A7, A16, A21, A36, RFUNCT_2: 21;

            then

             A37: 0 < ((f . x0) - fp) by XREAL_1: 50;

            (f . x0) < fm by A7, A11, A19, A36, RFUNCT_2: 21;

            then 0 < (fm - (f . x0)) by XREAL_1: 50;

            then 0 < R by A37, XXREAL_0: 15;

            then

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

            take N1;

            fp < fm by A17, A21, A19, A36, RFUNCT_2: 21;

            then [.fm, fp.] = {} by XXREAL_1: 29;

            then

             A38: ( [.fm, fp.] \/ [.fp, fm.]) = [.fp, fm.];

            thus N1 c= ( rng f1)

            proof

              let x be object;

              

               A39: ].fp, fm.[ c= [.fp, fm.] by XXREAL_1: 25;

              assume x in N1;

              then

              consider r2 such that

               A40: r2 = x and

               A41: ((f . x0) - R) < r2 and

               A42: r2 < ((f . x0) + R) by A6;

              R <= (fm - (f . x0)) by XXREAL_0: 17;

              then ((f . x0) + R) <= ((f . x0) + (fm - (f . x0))) by XREAL_1: 7;

              then

               A43: r2 < fm by A42, XXREAL_0: 2;

              R <= ((f . x0) - fp) by XXREAL_0: 17;

              then ((f . x0) - ((f . x0) - fp)) <= ((f . x0) - R) by XREAL_1: 13;

              then fp < r2 by A41, XXREAL_0: 2;

              then r2 in ].fp, fm.[ by A43;

              then

              consider s such that

               A44: s in [.(x0 - (r / 2)), (x0 + (r / 2)).] and

               A45: x = (f . s) by A1, A23, A24, A17, A38, A40, A39, FCONT_2: 15, XBOOLE_1: 1;

              s in N by A10, A22, A44;

              then s in (( dom f) /\ ].p, g.[) by A8, A14, XBOOLE_0:def 4;

              then

               A46: s in ( dom f1) by RELAT_1: 61;

              then x = (f1 . s) by A45, FUNCT_1: 47;

              hence thesis by A46, FUNCT_1:def 3;

            end;

          end;

        end;

        hence ex N be Neighbourhood of r1 st N c= ( rng f1);

      end;

      hence thesis by RCOMP_1: 20;

    end;

    theorem :: FCONT_3:24

    ( left_open_halfline p) c= ( dom f) & (f | ( left_open_halfline p)) is continuous & ((f | ( left_open_halfline p)) is increasing or (f | ( left_open_halfline p)) is decreasing) implies ( rng (f | ( left_open_halfline p))) is open

    proof

      set L = ( left_open_halfline p);

      assume that

       A1: ( left_open_halfline p) c= ( dom f) and

       A2: (f | L) is continuous and

       A3: (f | L) is increasing or (f | L) is decreasing;

      now

        let r1 be Element of REAL ;

        set f1 = (f | L);

        assume r1 in ( rng f1);

        then

        consider x0 be Element of REAL such that

         A4: x0 in ( dom f1) and

         A5: (f1 . x0) = r1 by PARTFUN1: 3;

        

         A6: r1 = (f . x0) by A4, A5, FUNCT_1: 47;

        

         A7: x0 in (( dom f) /\ L) by A4, RELAT_1: 61;

        then x0 in L by XBOOLE_0:def 4;

        then

        consider N be Neighbourhood of x0 such that

         A8: N c= L by RCOMP_1: 18;

        consider r be Real such that

         A9: 0 < r and

         A10: N = ].(x0 - r), (x0 + r).[ by RCOMP_1:def 6;

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

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

        then

         A11: (x0 - (r / 2)) < (x0 - 0 ) by XREAL_1: 15;

        

         A12: (r / 2) < r by A9, XREAL_1: 216;

        then

         A13: (x0 - r) < (x0 - (r / 2)) by XREAL_1: 15;

        

         A14: N c= ( dom f) by A1, A8;

        set fp = (f . (x0 + (r / 2)));

        set fm = (f . (x0 - (r / 2)));

        

         A15: (x0 + (r / 2)) < (x0 + r) by A12, XREAL_1: 8;

        

         A16: x0 < (x0 + (r / 2)) by A9, XREAL_1: 29, XREAL_1: 215;

        then

         A17: (x0 - (r / 2)) < (x0 + (r / 2)) by A11, XXREAL_0: 2;

        x0 < (x0 + r) by A9, XREAL_1: 29;

        then (x0 - (r / 2)) < (x0 + r) by A11, XXREAL_0: 2;

        then

         A18: (x0 - (r / 2)) in ].(x0 - r), (x0 + r).[ by A13;

        then

         A19: (x0 - (r / 2)) in (L /\ ( dom f)) by A8, A10, A14, XBOOLE_0:def 4;

        (x0 - r) < x0 by A9, XREAL_1: 44;

        then (x0 - r) < (x0 + (r / 2)) by A16, XXREAL_0: 2;

        then

         A20: (x0 + (r / 2)) in ].(x0 - r), (x0 + r).[ by A15;

        then

         A21: (x0 + (r / 2)) in (L /\ ( dom f)) by A8, A10, A14, XBOOLE_0:def 4;

        

         A22: [.(x0 - (r / 2)), (x0 + (r / 2)).] c= ].(x0 - r), (x0 + r).[ by A18, A20, XXREAL_2:def 12;

        (f | N) is continuous by A2, A8, FCONT_1: 16;

        then

         A23: (f | [.(x0 - (r / 2)), (x0 + (r / 2)).]) is continuous by A10, A22, FCONT_1: 16;

        

         A24: [.(x0 - (r / 2)), (x0 + (r / 2)).] c= L by A8, A10, A18, A20, XXREAL_2:def 12;

        now

          per cases by A3;

            suppose

             A25: (f | L) is increasing;

            set R = ( min (((f . x0) - fm),(fp - (f . x0))));

            (f . x0) < fp by A7, A16, A21, A25, RFUNCT_2: 20;

            then

             A26: 0 < (fp - (f . x0)) by XREAL_1: 50;

            fm < (f . x0) by A7, A11, A19, A25, RFUNCT_2: 20;

            then 0 < ((f . x0) - fm) by XREAL_1: 50;

            then 0 < R by A26, XXREAL_0: 15;

            then

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

            take N1;

            fm < fp by A17, A21, A19, A25, RFUNCT_2: 20;

            then [.fp, fm.] = {} by XXREAL_1: 29;

            then

             A27: ( [.fm, fp.] \/ [.fp, fm.]) = [.fm, fp.];

            thus N1 c= ( rng f1)

            proof

              let x be object;

              

               A28: ].fm, fp.[ c= [.fm, fp.] by XXREAL_1: 25;

              assume x in N1;

              then

              consider r2 such that

               A29: r2 = x and

               A30: ((f . x0) - R) < r2 and

               A31: r2 < ((f . x0) + R) by A6;

              R <= (fp - (f . x0)) by XXREAL_0: 17;

              then ((f . x0) + R) <= ((f . x0) + (fp - (f . x0))) by XREAL_1: 7;

              then

               A32: r2 < fp by A31, XXREAL_0: 2;

              R <= ((f . x0) - fm) by XXREAL_0: 17;

              then ((f . x0) - ((f . x0) - fm)) <= ((f . x0) - R) by XREAL_1: 13;

              then fm < r2 by A30, XXREAL_0: 2;

              then r2 in ].fm, fp.[ by A32;

              then

              consider s such that

               A33: s in [.(x0 - (r / 2)), (x0 + (r / 2)).] and

               A34: x = (f . s) by A1, A24, A23, A17, A27, A29, A28, FCONT_2: 15, XBOOLE_1: 1;

              s in N by A10, A22, A33;

              then s in (( dom f) /\ L) by A8, A14, XBOOLE_0:def 4;

              then

               A35: s in ( dom f1) by RELAT_1: 61;

              then x = (f1 . s) by A34, FUNCT_1: 47;

              hence thesis by A35, FUNCT_1:def 3;

            end;

          end;

            suppose

             A36: (f | L) is decreasing;

            set R = ( min ((fm - (f . x0)),((f . x0) - fp)));

            fp < (f . x0) by A7, A16, A21, A36, RFUNCT_2: 21;

            then

             A37: 0 < ((f . x0) - fp) by XREAL_1: 50;

            (f . x0) < fm by A7, A11, A19, A36, RFUNCT_2: 21;

            then 0 < (fm - (f . x0)) by XREAL_1: 50;

            then 0 < R by A37, XXREAL_0: 15;

            then

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

            take N1;

            fp < fm by A17, A21, A19, A36, RFUNCT_2: 21;

            then [.fm, fp.] = {} by XXREAL_1: 29;

            then

             A38: ( [.fm, fp.] \/ [.fp, fm.]) = [.fp, fm.];

            thus N1 c= ( rng f1)

            proof

              let x be object;

              

               A39: ].fp, fm.[ c= [.fp, fm.] by XXREAL_1: 25;

              assume x in N1;

              then

              consider r2 such that

               A40: r2 = x and

               A41: ((f . x0) - R) < r2 and

               A42: r2 < ((f . x0) + R) by A6;

              R <= (fm - (f . x0)) by XXREAL_0: 17;

              then ((f . x0) + R) <= ((f . x0) + (fm - (f . x0))) by XREAL_1: 7;

              then

               A43: r2 < fm by A42, XXREAL_0: 2;

              R <= ((f . x0) - fp) by XXREAL_0: 17;

              then ((f . x0) - ((f . x0) - fp)) <= ((f . x0) - R) by XREAL_1: 13;

              then fp < r2 by A41, XXREAL_0: 2;

              then r2 in ].fp, fm.[ by A43;

              then

              consider s such that

               A44: s in [.(x0 - (r / 2)), (x0 + (r / 2)).] and

               A45: x = (f . s) by A1, A24, A23, A17, A38, A40, A39, FCONT_2: 15, XBOOLE_1: 1;

              s in N by A10, A22, A44;

              then s in (( dom f) /\ L) by A8, A14, XBOOLE_0:def 4;

              then

               A46: s in ( dom f1) by RELAT_1: 61;

              then x = (f1 . s) by A45, FUNCT_1: 47;

              hence thesis by A46, FUNCT_1:def 3;

            end;

          end;

        end;

        hence ex N be Neighbourhood of r1 st N c= ( rng f1);

      end;

      hence thesis by RCOMP_1: 20;

    end;

    theorem :: FCONT_3:25

    ( right_open_halfline p) c= ( dom f) & (f | ( right_open_halfline p)) is continuous & ((f | ( right_open_halfline p)) is increasing or (f | ( right_open_halfline p)) is decreasing) implies ( rng (f | ( right_open_halfline p))) is open

    proof

      set L = ( right_open_halfline p);

      assume that

       A1: ( right_open_halfline p) c= ( dom f) and

       A2: (f | L) is continuous and

       A3: (f | L) is increasing or (f | L) is decreasing;

      now

        let r1 be Element of REAL ;

        set f1 = (f | L);

        assume r1 in ( rng f1);

        then

        consider x0 be Element of REAL such that

         A4: x0 in ( dom f1) and

         A5: (f1 . x0) = r1 by PARTFUN1: 3;

        

         A6: r1 = (f . x0) by A4, A5, FUNCT_1: 47;

        

         A7: x0 in (( dom f) /\ L) by A4, RELAT_1: 61;

        then x0 in L by XBOOLE_0:def 4;

        then

        consider N be Neighbourhood of x0 such that

         A8: N c= L by RCOMP_1: 18;

        consider r be Real such that

         A9: 0 < r and

         A10: N = ].(x0 - r), (x0 + r).[ by RCOMP_1:def 6;

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

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

        then

         A11: (x0 - (r / 2)) < (x0 - 0 ) by XREAL_1: 15;

        

         A12: (r / 2) < r by A9, XREAL_1: 216;

        then

         A13: (x0 - r) < (x0 - (r / 2)) by XREAL_1: 15;

        

         A14: N c= ( dom f) by A1, A8;

        set fp = (f . (x0 + (r / 2)));

        set fm = (f . (x0 - (r / 2)));

        

         A15: (x0 + (r / 2)) < (x0 + r) by A12, XREAL_1: 8;

        

         A16: x0 < (x0 + (r / 2)) by A9, XREAL_1: 29, XREAL_1: 215;

        then

         A17: (x0 - (r / 2)) < (x0 + (r / 2)) by A11, XXREAL_0: 2;

        x0 < (x0 + r) by A9, XREAL_1: 29;

        then (x0 - (r / 2)) < (x0 + r) by A11, XXREAL_0: 2;

        then

         A18: (x0 - (r / 2)) in ].(x0 - r), (x0 + r).[ by A13;

        then

         A19: (x0 - (r / 2)) in (L /\ ( dom f)) by A8, A10, A14, XBOOLE_0:def 4;

        (x0 - r) < x0 by A9, XREAL_1: 44;

        then (x0 - r) < (x0 + (r / 2)) by A16, XXREAL_0: 2;

        then

         A20: (x0 + (r / 2)) in ].(x0 - r), (x0 + r).[ by A15;

        then

         A21: (x0 + (r / 2)) in (L /\ ( dom f)) by A8, A10, A14, XBOOLE_0:def 4;

        

         A22: [.(x0 - (r / 2)), (x0 + (r / 2)).] c= ].(x0 - r), (x0 + r).[ by A18, A20, XXREAL_2:def 12;

        (f | N) is continuous by A2, A8, FCONT_1: 16;

        then

         A23: (f | [.(x0 - (r / 2)), (x0 + (r / 2)).]) is continuous by A10, A22, FCONT_1: 16;

        

         A24: [.(x0 - (r / 2)), (x0 + (r / 2)).] c= L by A8, A10, A18, A20, XXREAL_2:def 12;

        now

          per cases by A3;

            suppose

             A25: (f | L) is increasing;

            set R = ( min (((f . x0) - fm),(fp - (f . x0))));

            (f . x0) < fp by A7, A16, A21, A25, RFUNCT_2: 20;

            then

             A26: 0 < (fp - (f . x0)) by XREAL_1: 50;

            fm < (f . x0) by A7, A11, A19, A25, RFUNCT_2: 20;

            then 0 < ((f . x0) - fm) by XREAL_1: 50;

            then 0 < R by A26, XXREAL_0: 15;

            then

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

            take N1;

            fm < fp by A17, A21, A19, A25, RFUNCT_2: 20;

            then [.fp, fm.] = {} by XXREAL_1: 29;

            then

             A27: ( [.fm, fp.] \/ [.fp, fm.]) = [.fm, fp.];

            thus N1 c= ( rng f1)

            proof

              let x be object;

              

               A28: ].fm, fp.[ c= [.fm, fp.] by XXREAL_1: 25;

              assume x in N1;

              then

              consider r2 such that

               A29: r2 = x and

               A30: ((f . x0) - R) < r2 and

               A31: r2 < ((f . x0) + R) by A6;

              R <= (fp - (f . x0)) by XXREAL_0: 17;

              then ((f . x0) + R) <= ((f . x0) + (fp - (f . x0))) by XREAL_1: 7;

              then

               A32: r2 < fp by A31, XXREAL_0: 2;

              R <= ((f . x0) - fm) by XXREAL_0: 17;

              then ((f . x0) - ((f . x0) - fm)) <= ((f . x0) - R) by XREAL_1: 13;

              then fm < r2 by A30, XXREAL_0: 2;

              then r2 in ].fm, fp.[ by A32;

              then

              consider s such that

               A33: s in [.(x0 - (r / 2)), (x0 + (r / 2)).] and

               A34: x = (f . s) by A1, A24, A23, A17, A27, A29, A28, FCONT_2: 15, XBOOLE_1: 1;

              s in N by A10, A22, A33;

              then s in (( dom f) /\ L) by A8, A14, XBOOLE_0:def 4;

              then

               A35: s in ( dom f1) by RELAT_1: 61;

              then x = (f1 . s) by A34, FUNCT_1: 47;

              hence thesis by A35, FUNCT_1:def 3;

            end;

          end;

            suppose

             A36: (f | L) is decreasing;

            set R = ( min ((fm - (f . x0)),((f . x0) - fp)));

            fp < (f . x0) by A7, A16, A21, A36, RFUNCT_2: 21;

            then

             A37: 0 < ((f . x0) - fp) by XREAL_1: 50;

            (f . x0) < fm by A7, A11, A19, A36, RFUNCT_2: 21;

            then 0 < (fm - (f . x0)) by XREAL_1: 50;

            then 0 < R by A37, XXREAL_0: 15;

            then

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

            take N1;

            fp < fm by A17, A21, A19, A36, RFUNCT_2: 21;

            then [.fm, fp.] = {} by XXREAL_1: 29;

            then

             A38: ( [.fm, fp.] \/ [.fp, fm.]) = [.fp, fm.];

            thus N1 c= ( rng f1)

            proof

              let x be object;

              

               A39: ].fp, fm.[ c= [.fp, fm.] by XXREAL_1: 25;

              assume x in N1;

              then

              consider r2 such that

               A40: r2 = x and

               A41: ((f . x0) - R) < r2 and

               A42: r2 < ((f . x0) + R) by A6;

              R <= (fm - (f . x0)) by XXREAL_0: 17;

              then ((f . x0) + R) <= ((f . x0) + (fm - (f . x0))) by XREAL_1: 7;

              then

               A43: r2 < fm by A42, XXREAL_0: 2;

              R <= ((f . x0) - fp) by XXREAL_0: 17;

              then ((f . x0) - ((f . x0) - fp)) <= ((f . x0) - R) by XREAL_1: 13;

              then fp < r2 by A41, XXREAL_0: 2;

              then r2 in ].fp, fm.[ by A43;

              then

              consider s such that

               A44: s in [.(x0 - (r / 2)), (x0 + (r / 2)).] and

               A45: x = (f . s) by A1, A24, A23, A17, A38, A40, A39, FCONT_2: 15, XBOOLE_1: 1;

              s in N by A10, A22, A44;

              then s in (( dom f) /\ L) by A8, A14, XBOOLE_0:def 4;

              then

               A46: s in ( dom f1) by RELAT_1: 61;

              then x = (f1 . s) by A45, FUNCT_1: 47;

              hence thesis by A46, FUNCT_1:def 3;

            end;

          end;

        end;

        hence ex N be Neighbourhood of r1 st N c= ( rng f1);

      end;

      hence thesis by RCOMP_1: 20;

    end;

    theorem :: FCONT_3:26

    ( [#] REAL ) c= ( dom f) & (f | ( [#] REAL )) is continuous & ((f | ( [#] REAL )) is increasing or (f | ( [#] REAL )) is decreasing) implies ( rng f) is open

    proof

      set L = ( [#] REAL );

      assume that

       A1: ( [#] REAL ) c= ( dom f) and

       A2: (f | L) is continuous and

       A3: (f | L) is increasing or (f | L) is decreasing;

      now

        let r1 be Element of REAL ;

        assume r1 in ( rng f);

        then

        consider x0 be Element of REAL such that

         A4: x0 in ( dom f) and

         A5: (f . x0) = r1 by PARTFUN1: 3;

        

         A6: x0 in (L /\ ( dom f)) by A4, XBOOLE_0:def 4;

        set N = the Neighbourhood of x0;

        consider r be Real such that

         A7: 0 < r and

         A8: N = ].(x0 - r), (x0 + r).[ by RCOMP_1:def 6;

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

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

        then

         A9: (x0 - (r / 2)) < (x0 - 0 ) by XREAL_1: 15;

        

         A10: (r / 2) < r by A7, XREAL_1: 216;

        then

         A11: (x0 - r) < (x0 - (r / 2)) by XREAL_1: 15;

        

         A12: (x0 + (r / 2)) < (x0 + r) by A10, XREAL_1: 8;

        

         A13: N c= ( dom f) by A1;

        set fp = (f . (x0 + (r / 2)));

        set fm = (f . (x0 - (r / 2)));

        

         A14: (f | [.(x0 - (r / 2)), (x0 + (r / 2)).]) is continuous by A2, FCONT_1: 16;

        

         A15: x0 < (x0 + (r / 2)) by A7, XREAL_1: 29, XREAL_1: 215;

        then

         A16: (x0 - (r / 2)) < (x0 + (r / 2)) by A9, XXREAL_0: 2;

        (x0 - r) < x0 by A7, XREAL_1: 44;

        then (x0 - r) < (x0 + (r / 2)) by A15, XXREAL_0: 2;

        then

         A17: (x0 + (r / 2)) in ].(x0 - r), (x0 + r).[ by A12;

        then

         A18: (x0 + (r / 2)) in (L /\ ( dom f)) by A8, A13, XBOOLE_0:def 4;

        x0 < (x0 + r) by A7, XREAL_1: 29;

        then (x0 - (r / 2)) < (x0 + r) by A9, XXREAL_0: 2;

        then

         A19: (x0 - (r / 2)) in ].(x0 - r), (x0 + r).[ by A11;

        then

         A20: (x0 - (r / 2)) in (L /\ ( dom f)) by A8, A13, XBOOLE_0:def 4;

        

         A21: [.(x0 - (r / 2)), (x0 + (r / 2)).] c= ].(x0 - r), (x0 + r).[ by A19, A17, XXREAL_2:def 12;

        now

          per cases by A3;

            suppose

             A22: (f | L) is increasing;

            set R = ( min (((f . x0) - fm),(fp - (f . x0))));

            (f . x0) < fp by A15, A18, A6, A22, RFUNCT_2: 20;

            then

             A23: 0 < (fp - (f . x0)) by XREAL_1: 50;

            fm < (f . x0) by A9, A20, A6, A22, RFUNCT_2: 20;

            then 0 < ((f . x0) - fm) by XREAL_1: 50;

            then 0 < R by A23, XXREAL_0: 15;

            then

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

            take N1;

            fm < fp by A16, A18, A20, A22, RFUNCT_2: 20;

            then [.fp, fm.] = {} by XXREAL_1: 29;

            then

             A24: ( [.fm, fp.] \/ [.fp, fm.]) = [.fm, fp.];

            thus N1 c= ( rng f)

            proof

              let x be object;

              

               A25: [.(x0 - (r / 2)), (x0 + (r / 2)).] c= ( dom f) & ].fm, fp.[ c= [.fm, fp.] by A1, XXREAL_1: 25;

              assume x in N1;

              then

              consider r2 such that

               A26: r2 = x and

               A27: ((f . x0) - R) < r2 and

               A28: r2 < ((f . x0) + R) by A5;

              R <= (fp - (f . x0)) by XXREAL_0: 17;

              then ((f . x0) + R) <= ((f . x0) + (fp - (f . x0))) by XREAL_1: 7;

              then

               A29: r2 < fp by A28, XXREAL_0: 2;

              R <= ((f . x0) - fm) by XXREAL_0: 17;

              then ((f . x0) - ((f . x0) - fm)) <= ((f . x0) - R) by XREAL_1: 13;

              then fm < r2 by A27, XXREAL_0: 2;

              then r2 in ].fm, fp.[ by A29;

              then

              consider s such that

               A30: s in [.(x0 - (r / 2)), (x0 + (r / 2)).] and

               A31: x = (f . s) by A9, A15, A14, A24, A26, A25, FCONT_2: 15, XXREAL_0: 2;

              s in N by A8, A21, A30;

              hence thesis by A13, A31, FUNCT_1:def 3;

            end;

          end;

            suppose

             A32: (f | L) is decreasing;

            set R = ( min ((fm - (f . x0)),((f . x0) - fp)));

            fp < (f . x0) by A15, A18, A6, A32, RFUNCT_2: 21;

            then

             A33: 0 < ((f . x0) - fp) by XREAL_1: 50;

            (f . x0) < fm by A9, A20, A6, A32, RFUNCT_2: 21;

            then 0 < (fm - (f . x0)) by XREAL_1: 50;

            then 0 < R by A33, XXREAL_0: 15;

            then

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

            take N1;

            fp < fm by A16, A18, A20, A32, RFUNCT_2: 21;

            then [.fm, fp.] = {} by XXREAL_1: 29;

            then

             A34: ( [.fm, fp.] \/ [.fp, fm.]) = [.fp, fm.];

            thus N1 c= ( rng f)

            proof

              let x be object;

              

               A35: ].fp, fm.[ c= [.fp, fm.] by XXREAL_1: 25;

              assume x in N1;

              then

              consider r2 such that

               A36: r2 = x and

               A37: ((f . x0) - R) < r2 and

               A38: r2 < ((f . x0) + R) by A5;

              R <= (fm - (f . x0)) by XXREAL_0: 17;

              then ((f . x0) + R) <= ((f . x0) + (fm - (f . x0))) by XREAL_1: 7;

              then

               A39: r2 < fm by A38, XXREAL_0: 2;

              R <= ((f . x0) - fp) by XXREAL_0: 17;

              then ((f . x0) - ((f . x0) - fp)) <= ((f . x0) - R) by XREAL_1: 13;

              then fp < r2 by A37, XXREAL_0: 2;

              then r2 in ].fp, fm.[ by A39;

              then

              consider s such that

               A40: s in [.(x0 - (r / 2)), (x0 + (r / 2)).] and

               A41: x = (f . s) by A1, A14, A16, A34, A36, A35, FCONT_2: 15, XBOOLE_1: 1;

              s in N by A8, A21, A40;

              hence thesis by A13, A41, FUNCT_1:def 3;

            end;

          end;

        end;

        hence ex N be Neighbourhood of r1 st N c= ( rng f);

      end;

      hence thesis by RCOMP_1: 20;

    end;