:: FCONT_3 semantic presentation begin registration cluster [#] REAL -> closed ; coherence [#] REAL is closed proof let a be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng a c= [#] REAL or not a is convergent or lim a in [#] REAL ) thus ( not rng a c= [#] REAL or not a is convergent or lim a in [#] REAL ) ; ::_thesis: verum end; cluster empty -> closed for Element of K19(REAL); coherence for b1 being Subset of REAL st b1 is empty holds b1 is closed proof let S be Subset of REAL; ::_thesis: ( S is empty implies S is closed ) assume A1: S is empty ; ::_thesis: S is closed let a be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng a c= S or not a is convergent or lim a in S ) assume that A2: rng a c= S and a is convergent ; ::_thesis: lim a in S thus lim a in S by A1, A2, XBOOLE_1:3; ::_thesis: verum end; end; registration cluster [#] REAL -> open ; coherence [#] REAL is open proof ([#] REAL) ` = {} REAL by XBOOLE_1:37; hence [#] REAL is open by RCOMP_1:def_5; ::_thesis: verum end; cluster empty -> open for Element of K19(REAL); coherence for b1 being Subset of REAL st b1 is empty holds b1 is open proof let S be Subset of REAL; ::_thesis: ( S is empty implies S is open ) assume S is empty ; ::_thesis: S is open then S ` = [#] REAL ; hence S is open by RCOMP_1:def_5; ::_thesis: verum end; end; registration let r be real number ; cluster right_closed_halfline r -> closed ; coherence right_closed_halfline r is closed proof r in REAL by XREAL_0:def_1; then reconsider b = NAT --> r as Real_Sequence by FUNCOP_1:45; let a be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng a c= right_closed_halfline r or not a is convergent or lim a in right_closed_halfline r ) assume that A1: rng a c= right_closed_halfline r and A2: a is convergent ; ::_thesis: lim a in right_closed_halfline r A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_b_._n_<=_a_._n let n be Element of NAT ; ::_thesis: b . n <= a . 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 where g1 is Real : r <= g1 } by XXREAL_1:232; then ex r1 being Real st ( a . n = r1 & r <= r1 ) ; hence b . n <= a . n by FUNCOP_1:7; ::_thesis: verum end; lim b = b . 0 by SEQ_4:26 .= r by FUNCOP_1:7 ; then r <= lim a by A2, A3, SEQ_2:18; then lim a in { g1 where g1 is Real : r <= g1 } ; hence lim a in right_closed_halfline r by XXREAL_1:232; ::_thesis: verum end; cluster left_closed_halfline r -> closed ; coherence left_closed_halfline r is closed proof r in REAL by XREAL_0:def_1; then reconsider b = NAT --> r as Real_Sequence by FUNCOP_1:45; let a be Real_Sequence; :: according to RCOMP_1:def_4 ::_thesis: ( not rng a c= left_closed_halfline r or not a is convergent or lim a in left_closed_halfline r ) assume that A4: rng a c= left_closed_halfline r and A5: a is convergent ; ::_thesis: lim a in left_closed_halfline r A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_a_._n_<=_b_._n let n be Element of NAT ; ::_thesis: a . n <= b . 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 where g is Real : g <= r } by XXREAL_1:231; then ex r1 being Real st ( a . n = r1 & r1 <= r ) ; hence a . n <= b . n by FUNCOP_1:7; ::_thesis: verum end; lim b = b . 0 by SEQ_4:26 .= r by FUNCOP_1:7 ; then lim a <= r by A5, A6, SEQ_2:18; then lim a in { g1 where g1 is Real : g1 <= r } ; hence lim a in left_closed_halfline r by XXREAL_1:231; ::_thesis: verum end; cluster right_open_halfline r -> open ; coherence right_open_halfline r is open proof (right_open_halfline r) ` = left_closed_halfline r by XXREAL_1:224, XXREAL_1:296; hence right_open_halfline r is open by RCOMP_1:def_5; ::_thesis: verum end; cluster halfline r -> open ; coherence halfline r is open proof (left_open_halfline r) ` = right_closed_halfline r by XXREAL_1:224, XXREAL_1:290; hence halfline r is open by RCOMP_1:def_5; ::_thesis: verum end; end; theorem Th1: :: FCONT_3:1 for g, x0 being Real for r being real number st g in ].(x0 - r),(x0 + r).[ holds abs (g - x0) < r proof let g, x0 be Real; ::_thesis: for r being real number st g in ].(x0 - r),(x0 + r).[ holds abs (g - x0) < r let r be real number ; ::_thesis: ( g in ].(x0 - r),(x0 + r).[ implies abs (g - x0) < r ) assume g in ].(x0 - r),(x0 + r).[ ; ::_thesis: abs (g - x0) < r then A1: ex g1 being Real st ( g1 = g & x0 - r < g1 & g1 < x0 + r ) ; percases ( x0 <= g or g <= x0 ) ; supposeA2: x0 <= g ; ::_thesis: abs (g - x0) < r A3: g - x0 < (x0 + r) - x0 by A1, XREAL_1:14; 0 <= g - x0 by A2, XREAL_1:48; hence abs (g - x0) < r by A3, ABSVALUE:def_1; ::_thesis: verum end; suppose g <= x0 ; ::_thesis: abs (g - x0) < r then 0 <= x0 - g by XREAL_1:48; then A4: x0 - g = abs (- (g - x0)) by ABSVALUE:def_1 .= abs (g - x0) by COMPLEX1:52 ; x0 - g < x0 - (x0 - r) by A1, XREAL_1:15; hence abs (g - x0) < r by A4; ::_thesis: verum end; end; end; theorem :: FCONT_3:2 for g, x0 being Real for r being real number st g in ].(x0 - r),(x0 + r).[ holds g - x0 in ].(- r),r.[ proof let g, x0 be Real; ::_thesis: for r being real number st g in ].(x0 - r),(x0 + r).[ holds g - x0 in ].(- r),r.[ let r be real number ; ::_thesis: ( g in ].(x0 - r),(x0 + r).[ implies g - x0 in ].(- r),r.[ ) set r1 = g - x0; assume g in ].(x0 - r),(x0 + r).[ ; ::_thesis: g - x0 in ].(- r),r.[ then abs (g - x0) < r by Th1; then abs ((g - x0) - 0) < r ; then g - x0 in ].(0 - r),(0 + r).[ by RCOMP_1:1; hence g - x0 in ].(- r),r.[ ; ::_thesis: verum end; theorem Th3: :: FCONT_3:3 for g, x0, r1 being Real for r being real number st g = x0 + r1 & abs r1 < r holds ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) proof let g, x0, r1 be Real; ::_thesis: for r being real number st g = x0 + r1 & abs r1 < r holds ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) let r be real number ; ::_thesis: ( g = x0 + r1 & abs r1 < r implies ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) ) assume that A1: g = x0 + r1 and A2: abs r1 < r ; ::_thesis: ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) thus 0 < r by A2, COMPLEX1:46; ::_thesis: g in ].(x0 - r),(x0 + r).[ abs (g - x0) < r by A1, A2; hence g in ].(x0 - r),(x0 + r).[ by RCOMP_1:1; ::_thesis: verum end; theorem :: FCONT_3:4 for g, x0 being Real for r being real number st g - x0 in ].(- r),r.[ holds ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) proof let g, x0 be Real; ::_thesis: for r being real number st g - x0 in ].(- r),r.[ holds ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) let r be real number ; ::_thesis: ( g - x0 in ].(- r),r.[ implies ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) ) set r1 = g - x0; assume g - x0 in ].(- r),r.[ ; ::_thesis: ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) then ex g1 being Real st ( g1 = g - x0 & - r < g1 & g1 < r ) ; then A1: abs (g - x0) < r by SEQ_2:1; x0 + (g - x0) = g ; hence ( 0 < r & g in ].(x0 - r),(x0 + r).[ ) by A1, Th3; ::_thesis: verum end; theorem Th5: :: FCONT_3:5 for p being Real for a being Real_Sequence for x0 being real number st ( for n being Element of NAT holds a . n = x0 - (p / (n + 1)) ) holds ( a is convergent & lim a = x0 ) proof let p be Real; ::_thesis: for a being Real_Sequence for x0 being real number st ( for n being Element of NAT holds a . n = x0 - (p / (n + 1)) ) holds ( a is convergent & lim a = x0 ) let a be Real_Sequence; ::_thesis: for x0 being real number st ( for n being Element of NAT holds a . n = x0 - (p / (n + 1)) ) holds ( a is convergent & lim a = x0 ) let x0 be real number ; ::_thesis: ( ( for n being Element of NAT holds a . n = x0 - (p / (n + 1)) ) implies ( a is convergent & lim a = x0 ) ) deffunc H1( Element of NAT ) -> Element of REAL = p / ($1 + 1); consider d being Real_Sequence such that A1: for n being Element of NAT holds d . n = H1(n) from SEQ_1:sch_1(); x0 in REAL by XREAL_0:def_1; then reconsider b = NAT --> x0 as Real_Sequence by FUNCOP_1:45; assume A2: for n being Element of NAT holds a . n = x0 - (p / (n + 1)) ; ::_thesis: ( a is convergent & lim a = x0 ) now__::_thesis:_for_n_being_Element_of_NAT_holds_(b_-_d)_._n_=_a_._n let n be Element of NAT ; ::_thesis: (b - d) . n = a . n thus (b - d) . n = (b . n) - (d . n) by VALUED_1:15 .= x0 - (d . n) by FUNCOP_1:7 .= x0 - (p / (n + 1)) by A1 .= a . n by A2 ; ::_thesis: verum 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, SEQ_2:11; ::_thesis: lim a = x0 A5: lim b = b . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; lim d = 0 by A1, SEQ_4:31; hence lim a = x0 - 0 by A4, A5, A3, SEQ_2:12 .= x0 ; ::_thesis: verum end; theorem Th6: :: FCONT_3:6 for p being Real for a being Real_Sequence for x0 being real number st ( for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ) holds ( a is convergent & lim a = x0 ) proof let p be Real; ::_thesis: for a being Real_Sequence for x0 being real number st ( for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ) holds ( a is convergent & lim a = x0 ) let a be Real_Sequence; ::_thesis: for x0 being real number st ( for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ) holds ( a is convergent & lim a = x0 ) let x0 be real number ; ::_thesis: ( ( for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ) implies ( a is convergent & lim a = x0 ) ) deffunc H1( Element of NAT ) -> Element of REAL = p / ($1 + 1); consider d being Real_Sequence such that A1: for n being Element of NAT holds d . n = H1(n) from SEQ_1:sch_1(); x0 in REAL by XREAL_0:def_1; then reconsider b = NAT --> x0 as Real_Sequence by FUNCOP_1:45; assume A2: for n being Element of NAT holds a . n = x0 + (p / (n + 1)) ; ::_thesis: ( a is convergent & lim a = x0 ) now__::_thesis:_for_n_being_Element_of_NAT_holds_(b_+_d)_._n_=_a_._n let n be Element of NAT ; ::_thesis: (b + d) . n = a . n thus (b + d) . n = (b . n) + (d . n) by VALUED_1:1 .= x0 + (d . n) by FUNCOP_1:7 .= x0 + (p / (n + 1)) by A1 .= a . n by A2 ; ::_thesis: verum 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, SEQ_2:5; ::_thesis: lim a = x0 A5: lim b = b . 0 by SEQ_4:26 .= x0 by FUNCOP_1:7 ; lim d = 0 by A1, SEQ_4:31; hence lim a = x0 + 0 by A4, A5, A3, SEQ_2:6 .= x0 ; ::_thesis: verum end; theorem :: FCONT_3:7 for x0 being Real for r being real number for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> r & ex N being Neighbourhood of x0 st N c= dom f holds ex N being Neighbourhood of x0 st ( N c= dom f & ( for g being Real st g in N holds f . g <> r ) ) proof let x0 be Real; ::_thesis: for r being real number for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> r & ex N being Neighbourhood of x0 st N c= dom f holds ex N being Neighbourhood of x0 st ( N c= dom f & ( for g being Real st g in N holds f . g <> r ) ) let r be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f is_continuous_in x0 & f . x0 <> r & ex N being Neighbourhood of x0 st N c= dom f holds ex N being Neighbourhood of x0 st ( N c= dom f & ( for g being Real st g in N holds f . g <> r ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_continuous_in x0 & f . x0 <> r & ex N being Neighbourhood of x0 st N c= dom f implies ex N being Neighbourhood of x0 st ( N c= dom f & ( for g being Real st g in N holds f . g <> r ) ) ) assume that A1: f is_continuous_in x0 and A2: f . x0 <> r ; ::_thesis: ( for N being Neighbourhood of x0 holds not N c= dom f or ex N being Neighbourhood of x0 st ( N c= dom f & ( for g being Real st g in N holds f . g <> r ) ) ) given N being Neighbourhood of x0 such that A3: N c= dom f ; ::_thesis: ex N being Neighbourhood of x0 st ( N c= dom f & ( for g being Real st g in N holds f . g <> r ) ) consider p being real number such that A4: 0 < p and A5: N = ].(x0 - p),(x0 + p).[ by RCOMP_1:def_6; defpred S1[ Element of NAT , real number ] means ( x0 - (p / ($1 + 1)) < $2 & $2 < x0 + (p / ($1 + 1)) & f . $2 = r & $2 in dom f ); assume A6: for N being Neighbourhood of x0 holds ( not N c= dom f or ex g being Real st ( g in N & f . g = r ) ) ; ::_thesis: contradiction A7: for n being Element of NAT ex g being Real st S1[n,g] proof let n be Element of NAT ; ::_thesis: ex g being Real st S1[n,g] 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Nn or x in dom f ) assume x in Nn ; ::_thesis: x in dom f then consider g2 being Real 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 x in dom f by A3; ::_thesis: verum end; then consider g being Real such that A15: g in Nn and A16: f . g = r by A6; take g ; ::_thesis: S1[n,g] ex g1 being Real 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)) ) ; ::_thesis: ( f . g = r & g in dom f ) thus f . g = r by A16; ::_thesis: g in dom f thus g in dom f by A9, A15; ::_thesis: verum end; consider d being Real_Sequence such that A17: for n being Element of NAT holds S1[n,d . n] from FUNCT_2:sch_3(A7); A18: rng d c= dom f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng d or x in dom f ) assume x in rng d ; ::_thesis: x in dom f then ex n being Element of NAT st x = d . n by FUNCT_2:113; hence x in dom f by A17; ::_thesis: verum end; A19: now__::_thesis:_for_r2_being_real_number_st_0_<_r2_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_(((f_/*_d)_._m)_-_r)_<_r2 let r2 be real number ; ::_thesis: ( 0 < r2 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((f /* d) . m) - r) < r2 ) assume A20: 0 < r2 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((f /* d) . m) - r) < r2 take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds abs (((f /* d) . m) - r) < r2 let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((f /* d) . m) - r) < r2 ) assume n <= m ; ::_thesis: abs (((f /* d) . m) - r) < r2 abs (((f /* d) . m) - r) = abs ((f . (d . m)) - r) by A18, FUNCT_2:108 .= abs (r - r) by A17 .= 0 by ABSVALUE:2 ; hence abs (((f /* d) . m) - r) < r2 by A20; ::_thesis: verum end; deffunc H1( Element of NAT ) -> Element of REAL = x0 - (p / ($1 + 1)); consider a being Real_Sequence such that A21: for n being Element of NAT holds a . n = H1(n) from SEQ_1:sch_1(); deffunc H2( Element of NAT ) -> Element of REAL = x0 + (p / ($1 + 1)); consider b being Real_Sequence such that A22: for n being Element of NAT holds b . n = H2(n) from SEQ_1:sch_1(); A23: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_a_._n_<=_d_._n_&_d_._n_<=_b_._n_) let n be Element of NAT ; ::_thesis: ( a . n <= d . n & d . n <= b . n ) ( x0 - (p / (n + 1)) < d . n & d . n < x0 + (p / (n + 1)) ) by A17; hence ( a . n <= d . n & d . n <= b . n ) by A21, A22; ::_thesis: verum end; A24: p is Real by XREAL_0:def_1; then A25: ( b is convergent & lim b = x0 ) by A22, Th6; ( a is convergent & lim a = x0 ) by A24, A21, Th5; then ( d is convergent & lim d = x0 ) by A25, A23, 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; ::_thesis: verum end; theorem :: FCONT_3:8 for X being set for f being PartFunc of REAL,REAL st ( f | X is increasing or f | X is decreasing ) holds f | X is one-to-one proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st ( f | X is increasing or f | X is decreasing ) holds f | X is one-to-one let f be PartFunc of REAL,REAL; ::_thesis: ( ( f | X is increasing or f | X is decreasing ) implies f | X is one-to-one ) assume A1: ( f | X is increasing or f | X is decreasing ) ; ::_thesis: f | X is one-to-one now__::_thesis:_f_|_X_is_one-to-one percases ( f | X is increasing or f | X is decreasing ) by A1; supposeA2: f | X is increasing ; ::_thesis: f | X is one-to-one now__::_thesis:_for_r1,_r2_being_Real_holds_ (_not_r1_in_dom_(f_|_X)_or_not_r2_in_dom_(f_|_X)_or_not_(f_|_X)_._r1_=_(f_|_X)_._r2_or_not_r1_<>_r2_) given r1, r2 being 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 ; ::_thesis: contradiction A7: ( r1 in X /\ (dom f) & r2 in X /\ (dom f) ) by A3, A4, RELAT_1:61; now__::_thesis:_contradiction percases ( r1 < r2 or r2 < r1 ) by A6, XXREAL_0:1; suppose r1 < r2 ; ::_thesis: contradiction 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; ::_thesis: verum end; suppose r2 < r1 ; ::_thesis: contradiction 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; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence f | X is one-to-one by PARTFUN1:8; ::_thesis: verum end; supposeA8: f | X is decreasing ; ::_thesis: f | X is one-to-one now__::_thesis:_for_r1,_r2_being_Real_holds_ (_not_r1_in_dom_(f_|_X)_or_not_r2_in_dom_(f_|_X)_or_not_(f_|_X)_._r1_=_(f_|_X)_._r2_or_not_r1_<>_r2_) given r1, r2 being 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 ; ::_thesis: contradiction A13: ( r1 in X /\ (dom f) & r2 in X /\ (dom f) ) by A9, A10, RELAT_1:61; now__::_thesis:_contradiction percases ( r1 < r2 or r2 < r1 ) by A12, XXREAL_0:1; suppose r1 < r2 ; ::_thesis: contradiction 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; ::_thesis: verum end; suppose r2 < r1 ; ::_thesis: contradiction 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; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence f | X is one-to-one by PARTFUN1:8; ::_thesis: verum end; end; end; hence f | X is one-to-one ; ::_thesis: verum end; theorem Th9: :: FCONT_3:9 for X being set for f being one-to-one PartFunc of REAL,REAL st f | X is increasing holds ((f | X) ") | (f .: X) is increasing proof let X be set ; ::_thesis: for f being one-to-one PartFunc of REAL,REAL st f | X is increasing holds ((f | X) ") | (f .: X) is increasing let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( f | X is increasing implies ((f | X) ") | (f .: X) is increasing ) assume that A1: f | X is increasing and A2: not ((f | X) ") | (f .: X) is increasing ; ::_thesis: contradiction consider r1, r2 being Real 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__::_thesis:_contradiction percases ( ((f | X) ") . r1 = ((f | X) ") . r2 or ((f | X) ") . r1 <> ((f | X) ") . r2 ) ; suppose ((f | X) ") . r1 = ((f | X) ") . r2 ; ::_thesis: contradiction then r1 = (f | X) . (((f | X) ") . r2) by A8, FUNCT_1:35 .= r2 by A9, FUNCT_1:35 ; hence contradiction by A5; ::_thesis: verum end; supposeA11: ((f | X) ") . r1 <> ((f | X) ") . r2 ; ::_thesis: contradiction A12: dom (f | X) = dom ((f | X) | X) .= X /\ (dom (f | X)) by RELAT_1:61 ; 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; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem Th10: :: FCONT_3:10 for X being set for f being one-to-one PartFunc of REAL,REAL st f | X is decreasing holds ((f | X) ") | (f .: X) is decreasing proof let X be set ; ::_thesis: for f being one-to-one PartFunc of REAL,REAL st f | X is decreasing holds ((f | X) ") | (f .: X) is decreasing let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( f | X is decreasing implies ((f | X) ") | (f .: X) is decreasing ) assume that A1: f | X is decreasing and A2: not ((f | X) ") | (f .: X) is decreasing ; ::_thesis: contradiction consider r1, r2 being Real 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__::_thesis:_contradiction percases ( ((f | X) ") . r1 = ((f | X) ") . r2 or ((f | X) ") . r1 <> ((f | X) ") . r2 ) ; suppose ((f | X) ") . r1 = ((f | X) ") . r2 ; ::_thesis: contradiction then r1 = (f | X) . (((f | X) ") . r2) by A8, FUNCT_1:35 .= r2 by A9, FUNCT_1:35 ; hence contradiction by A5; ::_thesis: verum end; supposeA11: ((f | X) ") . r1 <> ((f | X) ") . r2 ; ::_thesis: contradiction A12: dom (f | X) = dom ((f | X) | X) .= X /\ (dom (f | X)) by RELAT_1:61 ; 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; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem Th11: :: FCONT_3:11 for X being set for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = left_open_halfline p holds f | X is continuous proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = left_open_halfline p holds f | X is continuous let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is monotone & ex p being Real st f .: X = left_open_halfline p implies f | X is continuous ) assume that A1: X c= dom f and A2: f | X is monotone ; ::_thesis: ( for p being Real holds not f .: X = left_open_halfline p or f | X is continuous ) given p being Real such that A3: f .: X = left_open_halfline p ; ::_thesis: f | X is continuous set L = left_open_halfline p; now__::_thesis:_f_|_X_is_continuous percases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def_5; suppose f | X is non-decreasing ; ::_thesis: f | X is continuous then A4: (f | X) | X is non-decreasing ; for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) A5: x0 in REAL by XREAL_0:def_1; A6: (f | X) .: X = f .: X by RELAT_1:129; assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 then x0 in X ; then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4; then A7: x0 in dom (f | X) by RELAT_1:61; then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6; then A8: (f | X) . x0 in left_open_halfline p by A3, RELAT_1:129; now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_ for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_ (f_|_X)_._x_in_N1 let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 consider N2 being Neighbourhood of (f | X) . x0 such that A9: N2 c= left_open_halfline p by A8, RCOMP_1:18; consider N3 being Neighbourhood of (f | X) . x0 such that A10: N3 c= N1 and A11: N3 c= N2 by RCOMP_1:17; consider r being real number such that A12: r > 0 and A13: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; 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: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A14; then ((f | X) . x0) + (r / 2) in N2 by A11, A13; then consider r2 being Real such that A18: ( r2 in dom (f | X) & r2 in X ) and A19: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A6, A9, PARTFUN2:59; A20: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A12, XREAL_1:29, XREAL_1:215; A21: now__::_thesis:_not_r2_<_x0 assume A22: r2 < x0 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A18, XBOOLE_0:def_4; hence contradiction by A4, A19, A20, A22, RFUNCT_2:22, A5; ::_thesis: verum 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: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A23; then ((f | X) . x0) - (r / 2) in N2 by A11, A13; then consider r1 being Real such that A25: ( r1 in dom (f | X) & r1 in X ) and A26: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A6, A9, PARTFUN2:59; A27: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A12, XREAL_1:29, XREAL_1:215; then A28: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19; A29: now__::_thesis:_not_x0_<_r1 assume A30: x0 < r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A25, XBOOLE_0:def_4; hence contradiction by A4, A26, A28, A30, RFUNCT_2:22, A5; ::_thesis: verum 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: min ((x0 - r1),(r2 - x0)) <= 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 min ((x0 - r1),(r2 - x0)) > 0 by A31, XXREAL_0:15; then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6; take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) A33: x in REAL by XREAL_0:def_1; assume that A34: x in dom (f | X) and A35: x in N ; ::_thesis: (f | X) . x in N1 A36: x in X /\ (dom (f | X)) by A34, XBOOLE_1:28; A37: ex s being Real st ( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A35; then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19; then A38: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9; min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17; then x0 - x < x0 - r1 by A38, XXREAL_0:2; then - (x0 - x) > - (x0 - r1) by XREAL_1:24; then A39: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6; r1 in X /\ (dom (f | X)) by A25, XBOOLE_0:def_4; then A40: (f | X) . r1 <= (f | X) . x by A4, A39, A36, RFUNCT_2:22, A33; x - x0 < min ((x0 - r1),(r2 - x0)) by A37, XREAL_1:19; then x - x0 < r2 - x0 by A32, XXREAL_0:2; then A41: (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 A4, A41, A36, RFUNCT_2:22, A33; then A42: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A26, A19, A40; [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A24, A17, XXREAL_2:def_12; then (f | X) . x in N3 by A13, A42; hence (f | X) . x in N1 by A10; ::_thesis: verum end; hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum end; hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum end; suppose f | X is non-increasing ; ::_thesis: f | X is continuous then A43: (f | X) | X is non-increasing ; for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) A44: x0 in REAL by XREAL_0:def_1; A45: (f | X) .: X = f .: X by RELAT_1:129; assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 then x0 in X ; then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4; then A46: x0 in dom (f | X) by RELAT_1:61; then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6; then A47: (f | X) . x0 in left_open_halfline p by A3, RELAT_1:129; now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_ for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_ (f_|_X)_._x_in_N1 let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 consider N2 being Neighbourhood of (f | X) . x0 such that A48: N2 c= left_open_halfline p by A47, RCOMP_1:18; consider N3 being Neighbourhood of (f | X) . x0 such that A49: N3 c= N1 and A50: N3 c= N2 by RCOMP_1:17; consider r being real number such that A51: r > 0 and A52: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; A53: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A51, XREAL_1:29, XREAL_1:215; set M2 = ((f | X) . x0) + (r / 2); A54: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A51, XREAL_1:29, XREAL_1:215; A55: (f | X) . x0 < ((f | X) . x0) + r by A51, 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 A54, XXREAL_0:2; then A56: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A53; then ((f | X) . x0) + (r / 2) in N2 by A50, A52; then consider r2 being Real such that A57: ( r2 in dom (f | X) & r2 in X ) and A58: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A45, A48, PARTFUN2:59; A59: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A51, XREAL_1:29, XREAL_1:215; A60: now__::_thesis:_not_r2_>_x0 assume A61: r2 > x0 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A46, A57, XBOOLE_0:def_4; hence contradiction by A43, A58, A59, A61, RFUNCT_2:23, A44; ::_thesis: verum end; set M1 = ((f | X) . x0) - (r / 2); A62: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A51, XREAL_1:29, XREAL_1:215; ((f | X) . x0) - (r / 2) < (f | X) . x0 by A54, XREAL_1:19; then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A55, XXREAL_0:2; then A63: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A62; then ((f | X) . x0) - (r / 2) in N2 by A50, A52; then consider r1 being Real such that A64: ( r1 in dom (f | X) & r1 in X ) and A65: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A45, A48, PARTFUN2:59; A66: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A51, XREAL_1:29, XREAL_1:215; then A67: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19; A68: now__::_thesis:_not_x0_>_r1 assume A69: x0 > r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A46, A64, XBOOLE_0:def_4; hence contradiction by A43, A65, A67, A69, RFUNCT_2:23, A44; ::_thesis: verum end; x0 <> r2 by A51, A58, XREAL_1:29, XREAL_1:215; then x0 > r2 by A60, XXREAL_0:1; then A70: x0 - r2 > 0 by XREAL_1:50; set R = min ((r1 - x0),(x0 - r2)); A71: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17; r1 <> x0 by A65, A66, XREAL_1:19; then r1 > x0 by A68, XXREAL_0:1; then r1 - x0 > 0 by XREAL_1:50; then min ((r1 - x0),(x0 - r2)) > 0 by A70, XXREAL_0:15; then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6; take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) A72: x in REAL by XREAL_0:def_1; assume that A73: x in dom (f | X) and A74: x in N ; ::_thesis: (f | X) . x in N1 A75: x in X /\ (dom (f | X)) by A73, XBOOLE_1:28; A76: ex s being Real st ( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A74; then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19; then A77: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9; x - x0 < min ((r1 - x0),(x0 - r2)) by A76, XREAL_1:19; then x - x0 < r1 - x0 by A71, XXREAL_0:2; then A78: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6; r1 in X /\ (dom (f | X)) by A64, XBOOLE_0:def_4; then A79: (f | X) . r1 <= (f | X) . x by A43, A78, A75, RFUNCT_2:23, A72; min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17; then x0 - x < x0 - r2 by A77, XXREAL_0:2; then - (x0 - x) > - (x0 - r2) by XREAL_1:24; then A80: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6; r2 in X /\ (dom (f | X)) by A57, XBOOLE_0:def_4; then (f | X) . x <= (f | X) . r2 by A43, A80, A75, RFUNCT_2:23, A72; then A81: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A65, A58, A79; [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A63, A56, XXREAL_2:def_12; then (f | X) . x in N3 by A52, A81; hence (f | X) . x in N1 by A49; ::_thesis: verum end; hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum end; hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum end; end; end; hence f | X is continuous ; ::_thesis: verum end; theorem Th12: :: FCONT_3:12 for X being set for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = right_open_halfline p holds f | X is continuous proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = right_open_halfline p holds f | X is continuous let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is monotone & ex p being Real st f .: X = right_open_halfline p implies f | X is continuous ) assume that A1: X c= dom f and A2: f | X is monotone ; ::_thesis: ( for p being Real holds not f .: X = right_open_halfline p or f | X is continuous ) given p being Real such that A3: f .: X = right_open_halfline p ; ::_thesis: f | X is continuous set L = right_open_halfline p; now__::_thesis:_f_|_X_is_continuous percases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def_5; suppose f | X is non-decreasing ; ::_thesis: f | X is continuous then A4: (f | X) | X is non-decreasing ; for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) A5: x0 in REAL by XREAL_0:def_1; A6: (f | X) .: X = f .: X by RELAT_1:129; assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 then x0 in X ; then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4; then A7: x0 in dom (f | X) by RELAT_1:61; then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6; then A8: (f | X) . x0 in right_open_halfline p by A3, RELAT_1:129; now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_ for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_ (f_|_X)_._x_in_N1 let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 consider N2 being Neighbourhood of (f | X) . x0 such that A9: N2 c= right_open_halfline p by A8, RCOMP_1:18; consider N3 being Neighbourhood of (f | X) . x0 such that A10: N3 c= N1 and A11: N3 c= N2 by RCOMP_1:17; consider r being real number such that A12: r > 0 and A13: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; 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: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A14; then ((f | X) . x0) + (r / 2) in N2 by A11, A13; then consider r2 being Real such that A18: ( r2 in dom (f | X) & r2 in X ) and A19: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A6, A9, PARTFUN2:59; A20: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A12, XREAL_1:29, XREAL_1:215; A21: now__::_thesis:_not_r2_<_x0 assume A22: r2 < x0 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A18, XBOOLE_0:def_4; hence contradiction by A4, A19, A20, A22, RFUNCT_2:22, A5; ::_thesis: verum 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: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A23; then ((f | X) . x0) - (r / 2) in N2 by A11, A13; then consider r1 being Real such that A25: ( r1 in dom (f | X) & r1 in X ) and A26: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A6, A9, PARTFUN2:59; A27: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A12, XREAL_1:29, XREAL_1:215; then A28: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19; A29: now__::_thesis:_not_x0_<_r1 assume A30: x0 < r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A25, XBOOLE_0:def_4; hence contradiction by A4, A26, A28, A30, RFUNCT_2:22, A5; ::_thesis: verum 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: min ((x0 - r1),(r2 - x0)) <= 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 min ((x0 - r1),(r2 - x0)) > 0 by A31, XXREAL_0:15; then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6; take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) A33: x in REAL by XREAL_0:def_1; assume that A34: x in dom (f | X) and A35: x in N ; ::_thesis: (f | X) . x in N1 A36: x in X /\ (dom (f | X)) by A34, XBOOLE_1:28; A37: ex s being Real st ( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A35; then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19; then A38: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9; min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17; then x0 - x < x0 - r1 by A38, XXREAL_0:2; then - (x0 - x) > - (x0 - r1) by XREAL_1:24; then A39: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6; r1 in X /\ (dom (f | X)) by A25, XBOOLE_0:def_4; then A40: (f | X) . r1 <= (f | X) . x by A4, A39, A36, RFUNCT_2:22, A33; x - x0 < min ((x0 - r1),(r2 - x0)) by A37, XREAL_1:19; then x - x0 < r2 - x0 by A32, XXREAL_0:2; then A41: (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 A4, A41, A36, RFUNCT_2:22, A33; then A42: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A26, A19, A40; [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A24, A17, XXREAL_2:def_12; then (f | X) . x in N3 by A13, A42; hence (f | X) . x in N1 by A10; ::_thesis: verum end; hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum end; hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum end; suppose f | X is non-increasing ; ::_thesis: f | X is continuous then A43: (f | X) | X is non-increasing ; for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) A44: x0 in REAL by XREAL_0:def_1; A45: (f | X) .: X = f .: X by RELAT_1:129; assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 then x0 in X ; then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4; then A46: x0 in dom (f | X) by RELAT_1:61; then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6; then A47: (f | X) . x0 in right_open_halfline p by A3, RELAT_1:129; now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_ for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_ (f_|_X)_._x_in_N1 let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 consider N2 being Neighbourhood of (f | X) . x0 such that A48: N2 c= right_open_halfline p by A47, RCOMP_1:18; consider N3 being Neighbourhood of (f | X) . x0 such that A49: N3 c= N1 and A50: N3 c= N2 by RCOMP_1:17; consider r being real number such that A51: r > 0 and A52: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; A53: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A51, XREAL_1:29, XREAL_1:215; set M2 = ((f | X) . x0) + (r / 2); A54: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A51, XREAL_1:29, XREAL_1:215; A55: (f | X) . x0 < ((f | X) . x0) + r by A51, 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 A54, XXREAL_0:2; then A56: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A53; then ((f | X) . x0) + (r / 2) in N2 by A50, A52; then consider r2 being Real such that A57: ( r2 in dom (f | X) & r2 in X ) and A58: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A45, A48, PARTFUN2:59; A59: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A51, XREAL_1:29, XREAL_1:215; A60: now__::_thesis:_not_r2_>_x0 assume A61: r2 > x0 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A46, A57, XBOOLE_0:def_4; hence contradiction by A43, A58, A59, A61, RFUNCT_2:23, A44; ::_thesis: verum end; set M1 = ((f | X) . x0) - (r / 2); A62: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A51, XREAL_1:29, XREAL_1:215; ((f | X) . x0) - (r / 2) < (f | X) . x0 by A54, XREAL_1:19; then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A55, XXREAL_0:2; then A63: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A62; then ((f | X) . x0) - (r / 2) in N2 by A50, A52; then consider r1 being Real such that A64: ( r1 in dom (f | X) & r1 in X ) and A65: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A45, A48, PARTFUN2:59; A66: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A51, XREAL_1:29, XREAL_1:215; then A67: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19; A68: now__::_thesis:_not_x0_>_r1 assume A69: x0 > r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A46, A64, XBOOLE_0:def_4; hence contradiction by A43, A65, A67, A69, RFUNCT_2:23, A44; ::_thesis: verum end; x0 <> r2 by A51, A58, XREAL_1:29, XREAL_1:215; then x0 > r2 by A60, XXREAL_0:1; then A70: x0 - r2 > 0 by XREAL_1:50; set R = min ((r1 - x0),(x0 - r2)); A71: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17; r1 <> x0 by A65, A66, XREAL_1:19; then r1 > x0 by A68, XXREAL_0:1; then r1 - x0 > 0 by XREAL_1:50; then min ((r1 - x0),(x0 - r2)) > 0 by A70, XXREAL_0:15; then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6; take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) A72: x in REAL by XREAL_0:def_1; assume that A73: x in dom (f | X) and A74: x in N ; ::_thesis: (f | X) . x in N1 A75: x in X /\ (dom (f | X)) by A73, XBOOLE_1:28; A76: ex s being Real st ( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A74; then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19; then A77: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9; x - x0 < min ((r1 - x0),(x0 - r2)) by A76, XREAL_1:19; then x - x0 < r1 - x0 by A71, XXREAL_0:2; then A78: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6; r1 in X /\ (dom (f | X)) by A64, XBOOLE_0:def_4; then A79: (f | X) . r1 <= (f | X) . x by A43, A78, A75, RFUNCT_2:23, A72; min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17; then x0 - x < x0 - r2 by A77, XXREAL_0:2; then - (x0 - x) > - (x0 - r2) by XREAL_1:24; then A80: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6; r2 in X /\ (dom (f | X)) by A57, XBOOLE_0:def_4; then (f | X) . x <= (f | X) . r2 by A43, A80, A75, RFUNCT_2:23, A72; then A81: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A65, A58, A79; [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A63, A56, XXREAL_2:def_12; then (f | X) . x in N3 by A52, A81; hence (f | X) . x in N1 by A49; ::_thesis: verum end; hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum end; hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum end; end; end; hence f | X is continuous ; ::_thesis: verum end; theorem Th13: :: FCONT_3:13 for X being set for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = left_closed_halfline p holds f | X is continuous proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = left_closed_halfline p holds f | X is continuous let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is monotone & ex p being Real st f .: X = left_closed_halfline p implies f | X is continuous ) assume that A1: X c= dom f and A2: f | X is monotone ; ::_thesis: ( for p being Real holds not f .: X = left_closed_halfline p or f | X is continuous ) given p being Real such that A3: f .: X = left_closed_halfline p ; ::_thesis: f | X is continuous set L = left_open_halfline p; set l = left_closed_halfline p; for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) A4: x0 in REAL by XREAL_0:def_1; A5: (f | X) .: X = f .: X by RELAT_1:129; A6: left_open_halfline p c= left_closed_halfline p by XXREAL_1:21; assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 then x0 in X ; then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4; then A7: 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} \/ (left_open_halfline p) by A3, A5, XXREAL_1:423; then A8: ( (f | X) . x0 in {p} or (f | X) . x0 in left_open_halfline p ) by XBOOLE_0:def_3; now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_ for_r1_being_real_number_st_r1_in_dom_(f_|_X)_&_r1_in_N_holds_ (f_|_X)_._r1_in_N1 let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st for r1 being real number st r1 in dom (f | X) & r1 in N holds (f | X) . r1 in N1 now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_ for_r1_being_real_number_st_r1_in_dom_(f_|_X)_&_r1_in_N_holds_ (f_|_X)_._r1_in_N1 percases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def_5; suppose f | X is non-decreasing ; ::_thesis: ex N being Neighbourhood of x0 st for r1 being real number st r1 in dom (f | X) & r1 in N holds (f | X) . r1 in N1 then A9: (f | X) | X is non-decreasing ; now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_ for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_ (f_|_X)_._x_in_N1 percases ( (f | X) . x0 in left_open_halfline p or (f | X) . x0 = p ) by A8, TARSKI:def_1; suppose (f | X) . x0 in left_open_halfline p ; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 then consider N2 being Neighbourhood of (f | X) . x0 such that A10: N2 c= left_open_halfline p by RCOMP_1:18; consider N3 being Neighbourhood of (f | X) . x0 such that A11: N3 c= N1 and A12: N3 c= N2 by RCOMP_1:17; consider r being real number such that A13: r > 0 and A14: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; A15: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A13, XREAL_1:29, XREAL_1:215; set M2 = ((f | X) . x0) + (r / 2); A16: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A13, XREAL_1:29, XREAL_1:215; A17: (f | X) . x0 < ((f | X) . x0) + r by A13, 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 A16, XXREAL_0:2; then A18: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A15; then ((f | X) . x0) + (r / 2) in N2 by A12, A14; then ((f | X) . x0) + (r / 2) in left_open_halfline p by A10; then consider r2 being Real such that A19: ( r2 in dom (f | X) & r2 in X ) and A20: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A5, A6, PARTFUN2:59; A21: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A13, XREAL_1:29, XREAL_1:215; A22: now__::_thesis:_not_r2_<_x0 assume A23: r2 < x0 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A19, XBOOLE_0:def_4; hence contradiction by A9, A20, A21, A23, RFUNCT_2:22, A4; ::_thesis: verum end; set M1 = ((f | X) . x0) - (r / 2); A24: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A13, XREAL_1:29, XREAL_1:215; ((f | X) . x0) - (r / 2) < (f | X) . x0 by A16, XREAL_1:19; then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A17, XXREAL_0:2; then A25: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A24; then ((f | X) . x0) - (r / 2) in N2 by A12, A14; then ((f | X) . x0) - (r / 2) in left_open_halfline p by A10; then consider r1 being Real such that A26: ( r1 in dom (f | X) & r1 in X ) and A27: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59; A28: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A13, XREAL_1:29, XREAL_1:215; then A29: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19; A30: now__::_thesis:_not_x0_<_r1 assume A31: x0 < r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A26, XBOOLE_0:def_4; hence contradiction by A9, A27, A29, A31, RFUNCT_2:22, A4; ::_thesis: verum end; x0 <> r2 by A13, A20, XREAL_1:29, XREAL_1:215; then x0 < r2 by A22, XXREAL_0:1; then A32: r2 - x0 > 0 by XREAL_1:50; set R = min ((x0 - r1),(r2 - x0)); A33: min ((x0 - r1),(r2 - x0)) <= r2 - x0 by XXREAL_0:17; r1 <> x0 by A27, A28, XREAL_1:19; then r1 < x0 by A30, XXREAL_0:1; then x0 - r1 > 0 by XREAL_1:50; then min ((x0 - r1),(r2 - x0)) > 0 by A32, XXREAL_0:15; then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6; take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) A34: x in REAL by XREAL_0:def_1; assume that A35: x in dom (f | X) and A36: x in N ; ::_thesis: (f | X) . x in N1 A37: x in X /\ (dom (f | X)) by A35, XBOOLE_1:28; A38: ex s being Real st ( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A36; then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19; then A39: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9; min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17; then x0 - x < x0 - r1 by A39, XXREAL_0:2; then - (x0 - x) > - (x0 - r1) by XREAL_1:24; then A40: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6; r1 in X /\ (dom (f | X)) by A26, XBOOLE_0:def_4; then A41: (f | X) . r1 <= (f | X) . x by A9, A40, A37, RFUNCT_2:22, A34; x - x0 < min ((x0 - r1),(r2 - x0)) by A38, XREAL_1:19; then x - x0 < r2 - x0 by A33, XXREAL_0:2; then A42: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:6; r2 in X /\ (dom (f | X)) by A19, XBOOLE_0:def_4; then (f | X) . x <= (f | X) . r2 by A9, A42, A37, RFUNCT_2:22, A34; then A43: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A27, A20, A41; [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A25, A18, XXREAL_2:def_12; then (f | X) . x in N3 by A14, A43; hence (f | X) . x in N1 by A11; ::_thesis: verum end; supposeA44: (f | X) . x0 = p ; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 then consider r being real number such that A45: r > 0 and A46: N1 = ].(p - r),(p + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; set R = r / 2; A47: p < p + (r / 2) by A45, XREAL_1:29, XREAL_1:215; A48: p - (r / 2) < p by A45, XREAL_1:44, XREAL_1:215; then p - (r / 2) in { s where s is Real : s < p } ; then p - (r / 2) in left_open_halfline p by XXREAL_1:229; then consider r1 being Real such that A49: ( r1 in dom (f | X) & r1 in X ) and A50: p - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59; A51: r1 in X /\ (dom (f | X)) by A49, XBOOLE_0:def_4; A52: now__::_thesis:_not_x0_<_r1 assume A53: x0 < r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A49, XBOOLE_0:def_4; hence contradiction by A9, A44, A48, A50, A53, RFUNCT_2:22, A4; ::_thesis: verum end; r1 <> x0 by A44, A45, A50, XREAL_1:44, XREAL_1:215; then r1 < x0 by A52, 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 = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) assume that A54: x in dom (f | X) and A55: x in N ; ::_thesis: (f | X) . x in N1 A56: ex s being Real st ( s = x & x0 - (x0 - r1) < s & s < x0 + (x0 - r1) ) by A55; A57: r / 2 < r by A45, XREAL_1:216; then A58: p - r < p - (r / 2) by XREAL_1:15; (f | X) . x in left_closed_halfline p by A3, A5, A54, FUNCT_1:def_6; then (f | X) . x in { s where s is Real : s <= p } by XXREAL_1:231; then ex s being Real st ( s = (f | X) . x & s <= p ) ; then A59: (f | X) . x <= p + (r / 2) by A47, XXREAL_0:2; x in X /\ (dom (f | X)) by A54, XBOOLE_0:def_4; then p - (r / 2) <= (f | X) . x by A9, A50, A51, A56, RFUNCT_2:22; then A60: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A59; p < p + r by A45, XREAL_1:29; then p - (r / 2) < p + r by A48, XXREAL_0:2; then A61: p - (r / 2) in ].(p - r),(p + r).[ by A58; A62: p + (r / 2) < p + r by A57, XREAL_1:6; p - r < p by A45, XREAL_1:44; then p - r < p + (r / 2) by A47, XXREAL_0:2; then p + (r / 2) in ].(p - r),(p + r).[ by A62; then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A46, A61, XXREAL_2:def_12; hence (f | X) . x in N1 by A60; ::_thesis: verum end; end; end; hence ex N being Neighbourhood of x0 st for r1 being real number st r1 in dom (f | X) & r1 in N holds (f | X) . r1 in N1 ; ::_thesis: verum end; suppose f | X is non-increasing ; ::_thesis: ex N being Neighbourhood of x0 st for r1 being real number st r1 in dom (f | X) & r1 in N holds (f | X) . r1 in N1 then A63: (f | X) | X is non-increasing ; now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_ for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_ (f_|_X)_._x_in_N1 percases ( (f | X) . x0 in left_open_halfline p or (f | X) . x0 = p ) by A8, TARSKI:def_1; suppose (f | X) . x0 in left_open_halfline p ; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 then consider N2 being Neighbourhood of (f | X) . x0 such that A64: N2 c= left_open_halfline p by RCOMP_1:18; consider N3 being Neighbourhood of (f | X) . x0 such that A65: N3 c= N1 and A66: N3 c= N2 by RCOMP_1:17; consider r being real number such that A67: r > 0 and A68: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; A69: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A67, XREAL_1:29, XREAL_1:215; set M2 = ((f | X) . x0) + (r / 2); A70: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A67, XREAL_1:29, XREAL_1:215; A71: (f | X) . x0 < ((f | X) . x0) + r by A67, 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 A70, XXREAL_0:2; then A72: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A69; then ((f | X) . x0) + (r / 2) in N2 by A66, A68; then ((f | X) . x0) + (r / 2) in left_open_halfline p by A64; then consider r2 being Real such that A73: ( r2 in dom (f | X) & r2 in X ) and A74: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A5, A6, PARTFUN2:59; A75: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A67, XREAL_1:29, XREAL_1:215; A76: now__::_thesis:_not_r2_>_x0 assume A77: r2 > x0 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A73, XBOOLE_0:def_4; hence contradiction by A63, A74, A75, A77, RFUNCT_2:23, A4; ::_thesis: verum end; set M1 = ((f | X) . x0) - (r / 2); A78: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A67, XREAL_1:29, XREAL_1:215; ((f | X) . x0) - (r / 2) < (f | X) . x0 by A70, XREAL_1:19; then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A71, XXREAL_0:2; then A79: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A78; then ((f | X) . x0) - (r / 2) in N2 by A66, A68; then ((f | X) . x0) - (r / 2) in left_open_halfline p by A64; then consider r1 being Real such that A80: ( r1 in dom (f | X) & r1 in X ) and A81: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59; A82: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A67, XREAL_1:29, XREAL_1:215; then A83: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19; A84: now__::_thesis:_not_x0_>_r1 assume A85: x0 > r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A80, XBOOLE_0:def_4; hence contradiction by A63, A81, A83, A85, RFUNCT_2:23, A4; ::_thesis: verum end; x0 <> r2 by A67, A74, XREAL_1:29, XREAL_1:215; then x0 > r2 by A76, XXREAL_0:1; then A86: x0 - r2 > 0 by XREAL_1:50; set R = min ((r1 - x0),(x0 - r2)); A87: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17; r1 <> x0 by A81, A82, XREAL_1:19; then r1 > x0 by A84, XXREAL_0:1; then r1 - x0 > 0 by XREAL_1:50; then min ((r1 - x0),(x0 - r2)) > 0 by A86, XXREAL_0:15; then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6; take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) A88: x in REAL by XREAL_0:def_1; assume that A89: x in dom (f | X) and A90: x in N ; ::_thesis: (f | X) . x in N1 A91: x in X /\ (dom (f | X)) by A89, XBOOLE_1:28; A92: ex s being Real st ( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A90; then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19; then A93: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9; x - x0 < min ((r1 - x0),(x0 - r2)) by A92, XREAL_1:19; then x - x0 < r1 - x0 by A87, XXREAL_0:2; then A94: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6; r1 in X /\ (dom (f | X)) by A80, XBOOLE_0:def_4; then A95: (f | X) . r1 <= (f | X) . x by A63, A94, A91, RFUNCT_2:23, A88; min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17; then x0 - x < x0 - r2 by A93, XXREAL_0:2; then - (x0 - x) > - (x0 - r2) by XREAL_1:24; then A96: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6; r2 in X /\ (dom (f | X)) by A73, XBOOLE_0:def_4; then (f | X) . x <= (f | X) . r2 by A63, A96, A91, RFUNCT_2:23, A88; then A97: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A81, A74, A95; [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A79, A72, XXREAL_2:def_12; then (f | X) . x in N3 by A68, A97; hence (f | X) . x in N1 by A65; ::_thesis: verum end; supposeA98: (f | X) . x0 = p ; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 then consider r being real number such that A99: r > 0 and A100: N1 = ].(p - r),(p + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; set R = r / 2; A101: p < p + (r / 2) by A99, XREAL_1:29, XREAL_1:215; A102: p - (r / 2) < p by A99, XREAL_1:44, XREAL_1:215; then p - (r / 2) in { s where s is Real : s < p } ; then p - (r / 2) in left_open_halfline p by XXREAL_1:229; then consider r1 being Real such that A103: ( r1 in dom (f | X) & r1 in X ) and A104: p - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59; A105: r1 in X /\ (dom (f | X)) by A103, XBOOLE_0:def_4; A106: now__::_thesis:_not_x0_>_r1 assume A107: x0 > r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A103, XBOOLE_0:def_4; hence contradiction by A63, A98, A102, A104, A107, RFUNCT_2:23, A4; ::_thesis: verum end; r1 <> x0 by A98, A99, A104, XREAL_1:44, XREAL_1:215; then r1 > x0 by A106, 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 = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) assume that A108: x in dom (f | X) and A109: x in N ; ::_thesis: (f | X) . x in N1 A110: ex s being Real st ( s = x & x0 - (r1 - x0) < s & s < x0 + (r1 - x0) ) by A109; A111: r / 2 < r by A99, XREAL_1:216; then A112: p - r < p - (r / 2) by XREAL_1:15; (f | X) . x in left_closed_halfline p by A3, A5, A108, FUNCT_1:def_6; then (f | X) . x in { s where s is Real : s <= p } by XXREAL_1:231; then ex s being Real st ( s = (f | X) . x & s <= p ) ; then A113: (f | X) . x <= p + (r / 2) by A101, XXREAL_0:2; x in X /\ (dom (f | X)) by A108, XBOOLE_0:def_4; then p - (r / 2) <= (f | X) . x by A63, A104, A105, A110, RFUNCT_2:23; then A114: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A113; p < p + r by A99, XREAL_1:29; then p - (r / 2) < p + r by A102, XXREAL_0:2; then A115: p - (r / 2) in ].(p - r),(p + r).[ by A112; A116: p + (r / 2) < p + r by A111, XREAL_1:6; p - r < p by A99, XREAL_1:44; then p - r < p + (r / 2) by A101, XXREAL_0:2; then p + (r / 2) in ].(p - r),(p + r).[ by A116; then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A100, A115, XXREAL_2:def_12; hence (f | X) . x in N1 by A114; ::_thesis: verum end; end; end; hence ex N being Neighbourhood of x0 st for r1 being real number st r1 in dom (f | X) & r1 in N holds (f | X) . r1 in N1 ; ::_thesis: verum end; end; end; hence ex N being Neighbourhood of x0 st for r1 being real number st r1 in dom (f | X) & r1 in N holds (f | X) . r1 in N1 ; ::_thesis: verum end; hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum end; hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum end; theorem Th14: :: FCONT_3:14 for X being set for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = right_closed_halfline p holds f | X is continuous proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p being Real st f .: X = right_closed_halfline p holds f | X is continuous let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is monotone & ex p being Real st f .: X = right_closed_halfline p implies f | X is continuous ) assume that A1: X c= dom f and A2: f | X is monotone ; ::_thesis: ( for p being Real holds not f .: X = right_closed_halfline p or f | X is continuous ) given p being Real such that A3: f .: X = right_closed_halfline p ; ::_thesis: f | X is continuous set L = right_open_halfline p; set l = right_closed_halfline p; for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) A4: x0 in REAL by XREAL_0:def_1; A5: (f | X) .: X = f .: X by RELAT_1:129; A6: right_open_halfline p c= right_closed_halfline p by XXREAL_1:22; assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 then x0 in X ; then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4; then A7: 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} \/ (right_open_halfline p) by A3, A5, XXREAL_1:427; then A8: ( (f | X) . x0 in {p} or (f | X) . x0 in right_open_halfline p ) by XBOOLE_0:def_3; now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_ for_r1_being_real_number_st_r1_in_dom_(f_|_X)_&_r1_in_N_holds_ (f_|_X)_._r1_in_N1 let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st for r1 being real number st r1 in dom (f | X) & r1 in N holds (f | X) . r1 in N1 now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_ for_r1_being_real_number_st_r1_in_dom_(f_|_X)_&_r1_in_N_holds_ (f_|_X)_._r1_in_N1 percases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def_5; suppose f | X is non-decreasing ; ::_thesis: ex N being Neighbourhood of x0 st for r1 being real number st r1 in dom (f | X) & r1 in N holds (f | X) . r1 in N1 then A9: (f | X) | X is non-decreasing ; now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_ for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_ (f_|_X)_._x_in_N1 percases ( (f | X) . x0 in right_open_halfline p or (f | X) . x0 = p ) by A8, TARSKI:def_1; suppose (f | X) . x0 in right_open_halfline p ; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 then consider N2 being Neighbourhood of (f | X) . x0 such that A10: N2 c= right_open_halfline p by RCOMP_1:18; consider N3 being Neighbourhood of (f | X) . x0 such that A11: N3 c= N1 and A12: N3 c= N2 by RCOMP_1:17; consider r being real number such that A13: r > 0 and A14: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; A15: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A13, XREAL_1:29, XREAL_1:215; set M2 = ((f | X) . x0) + (r / 2); A16: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A13, XREAL_1:29, XREAL_1:215; A17: (f | X) . x0 < ((f | X) . x0) + r by A13, 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 A16, XXREAL_0:2; then A18: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A15; then ((f | X) . x0) + (r / 2) in N2 by A12, A14; then ((f | X) . x0) + (r / 2) in right_open_halfline p by A10; then consider r2 being Real such that A19: ( r2 in dom (f | X) & r2 in X ) and A20: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A5, A6, PARTFUN2:59; A21: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A13, XREAL_1:29, XREAL_1:215; A22: now__::_thesis:_not_r2_<_x0 assume A23: r2 < x0 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A19, XBOOLE_0:def_4; hence contradiction by A9, A20, A21, A23, RFUNCT_2:22, A4; ::_thesis: verum end; set M1 = ((f | X) . x0) - (r / 2); A24: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A13, XREAL_1:29, XREAL_1:215; ((f | X) . x0) - (r / 2) < (f | X) . x0 by A16, XREAL_1:19; then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A17, XXREAL_0:2; then A25: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A24; then ((f | X) . x0) - (r / 2) in N2 by A12, A14; then ((f | X) . x0) - (r / 2) in right_open_halfline p by A10; then consider r1 being Real such that A26: ( r1 in dom (f | X) & r1 in X ) and A27: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59; A28: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A13, XREAL_1:29, XREAL_1:215; then A29: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19; A30: now__::_thesis:_not_x0_<_r1 assume A31: x0 < r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A26, XBOOLE_0:def_4; hence contradiction by A9, A27, A29, A31, RFUNCT_2:22, A4; ::_thesis: verum end; x0 <> r2 by A13, A20, XREAL_1:29, XREAL_1:215; then x0 < r2 by A22, XXREAL_0:1; then A32: r2 - x0 > 0 by XREAL_1:50; set R = min ((x0 - r1),(r2 - x0)); A33: min ((x0 - r1),(r2 - x0)) <= r2 - x0 by XXREAL_0:17; r1 <> x0 by A27, A28, XREAL_1:19; then r1 < x0 by A30, XXREAL_0:1; then x0 - r1 > 0 by XREAL_1:50; then min ((x0 - r1),(r2 - x0)) > 0 by A32, XXREAL_0:15; then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6; take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) A34: x in REAL by XREAL_0:def_1; assume that A35: x in dom (f | X) and A36: x in N ; ::_thesis: (f | X) . x in N1 A37: x in X /\ (dom (f | X)) by A35, XBOOLE_1:28; A38: ex s being Real st ( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A36; then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19; then A39: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9; min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17; then x0 - x < x0 - r1 by A39, XXREAL_0:2; then - (x0 - x) > - (x0 - r1) by XREAL_1:24; then A40: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6; r1 in X /\ (dom (f | X)) by A26, XBOOLE_0:def_4; then A41: (f | X) . r1 <= (f | X) . x by A9, A40, A37, RFUNCT_2:22, A34; x - x0 < min ((x0 - r1),(r2 - x0)) by A38, XREAL_1:19; then x - x0 < r2 - x0 by A33, XXREAL_0:2; then A42: (x - x0) + x0 < (r2 - x0) + x0 by XREAL_1:6; r2 in X /\ (dom (f | X)) by A19, XBOOLE_0:def_4; then (f | X) . x <= (f | X) . r2 by A9, A42, A37, RFUNCT_2:22, A34; then A43: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A27, A20, A41; [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A25, A18, XXREAL_2:def_12; then (f | X) . x in N3 by A14, A43; hence (f | X) . x in N1 by A11; ::_thesis: verum end; supposeA44: (f | X) . x0 = p ; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 then consider r being real number such that A45: r > 0 and A46: N1 = ].(p - r),(p + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; set R = r / 2; A47: p - (r / 2) < p by A45, XREAL_1:44, XREAL_1:215; A48: p < p + (r / 2) by A45, XREAL_1:29, XREAL_1:215; then p + (r / 2) in { s where s is Real : p < s } ; then p + (r / 2) in right_open_halfline p by XXREAL_1:230; then consider r1 being Real such that A49: ( r1 in dom (f | X) & r1 in X ) and A50: p + (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59; A51: now__::_thesis:_not_x0_>_r1 assume A52: x0 > r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A49, XBOOLE_0:def_4; hence contradiction by A9, A44, A48, A50, A52, RFUNCT_2:22, A4; ::_thesis: verum end; r1 <> x0 by A44, A45, A50, XREAL_1:29, XREAL_1:215; then r1 > x0 by A51, 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 = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) assume that A53: x in dom (f | X) and A54: x in N ; ::_thesis: (f | X) . x in N1 A55: ex s being Real st ( s = x & x0 - (r1 - x0) < s & s < x0 + (r1 - x0) ) by A54; (f | X) . x in right_closed_halfline p by A3, A5, A53, FUNCT_1:def_6; then (f | X) . x in { s where s is Real : p <= s } by XXREAL_1:232; then ex s being Real st ( s = (f | X) . x & p <= s ) ; then A56: p - (r / 2) <= (f | X) . x by A47, XXREAL_0:2; A57: r1 in X /\ (dom (f | X)) by A49, XBOOLE_0:def_4; x in X /\ (dom (f | X)) by A53, XBOOLE_0:def_4; then p + (r / 2) >= (f | X) . x by A9, A50, A57, A55, RFUNCT_2:22; then A58: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A56; A59: r / 2 < r by A45, XREAL_1:216; then A60: p - r < p - (r / 2) by XREAL_1:15; p < p + r by A45, XREAL_1:29; then p - (r / 2) < p + r by A47, XXREAL_0:2; then A61: p - (r / 2) in ].(p - r),(p + r).[ by A60; A62: p + (r / 2) < p + r by A59, XREAL_1:6; p - r < p by A45, XREAL_1:44; then p - r < p + (r / 2) by A48, XXREAL_0:2; then p + (r / 2) in ].(p - r),(p + r).[ by A62; then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A46, A61, XXREAL_2:def_12; hence (f | X) . x in N1 by A58; ::_thesis: verum end; end; end; hence ex N being Neighbourhood of x0 st for r1 being real number st r1 in dom (f | X) & r1 in N holds (f | X) . r1 in N1 ; ::_thesis: verum end; suppose f | X is non-increasing ; ::_thesis: ex N being Neighbourhood of x0 st for r1 being real number st r1 in dom (f | X) & r1 in N holds (f | X) . r1 in N1 then A63: (f | X) | X is non-increasing ; now__::_thesis:_ex_N_being_Neighbourhood_of_x0_st_ for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_ (f_|_X)_._x_in_N1 percases ( (f | X) . x0 in right_open_halfline p or (f | X) . x0 = p ) by A8, TARSKI:def_1; suppose (f | X) . x0 in right_open_halfline p ; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 then consider N2 being Neighbourhood of (f | X) . x0 such that A64: N2 c= right_open_halfline p by RCOMP_1:18; consider N3 being Neighbourhood of (f | X) . x0 such that A65: N3 c= N1 and A66: N3 c= N2 by RCOMP_1:17; consider r being real number such that A67: r > 0 and A68: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; A69: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A67, XREAL_1:29, XREAL_1:215; set M2 = ((f | X) . x0) + (r / 2); A70: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A67, XREAL_1:29, XREAL_1:215; A71: (f | X) . x0 < ((f | X) . x0) + r by A67, 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 A70, XXREAL_0:2; then A72: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A69; then ((f | X) . x0) + (r / 2) in N2 by A66, A68; then ((f | X) . x0) + (r / 2) in right_open_halfline p by A64; then consider r2 being Real such that A73: ( r2 in dom (f | X) & r2 in X ) and A74: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A5, A6, PARTFUN2:59; A75: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A67, XREAL_1:29, XREAL_1:215; A76: now__::_thesis:_not_r2_>_x0 assume A77: r2 > x0 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A73, XBOOLE_0:def_4; hence contradiction by A63, A74, A75, A77, RFUNCT_2:23, A4; ::_thesis: verum end; set M1 = ((f | X) . x0) - (r / 2); A78: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A67, XREAL_1:29, XREAL_1:215; ((f | X) . x0) - (r / 2) < (f | X) . x0 by A70, XREAL_1:19; then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A71, XXREAL_0:2; then A79: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A78; then ((f | X) . x0) - (r / 2) in N2 by A66, A68; then ((f | X) . x0) - (r / 2) in right_open_halfline p by A64; then consider r1 being Real such that A80: ( r1 in dom (f | X) & r1 in X ) and A81: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59; A82: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A67, XREAL_1:29, XREAL_1:215; then A83: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19; A84: now__::_thesis:_not_x0_>_r1 assume A85: x0 > r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A80, XBOOLE_0:def_4; hence contradiction by A63, A81, A83, A85, RFUNCT_2:23, A4; ::_thesis: verum end; x0 <> r2 by A67, A74, XREAL_1:29, XREAL_1:215; then x0 > r2 by A76, XXREAL_0:1; then A86: x0 - r2 > 0 by XREAL_1:50; set R = min ((r1 - x0),(x0 - r2)); A87: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17; r1 <> x0 by A81, A82, XREAL_1:19; then r1 > x0 by A84, XXREAL_0:1; then r1 - x0 > 0 by XREAL_1:50; then min ((r1 - x0),(x0 - r2)) > 0 by A86, XXREAL_0:15; then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6; take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) A88: x in REAL by XREAL_0:def_1; assume that A89: x in dom (f | X) and A90: x in N ; ::_thesis: (f | X) . x in N1 A91: x in X /\ (dom (f | X)) by A89, XBOOLE_1:28; A92: ex s being Real st ( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A90; then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19; then A93: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9; x - x0 < min ((r1 - x0),(x0 - r2)) by A92, XREAL_1:19; then x - x0 < r1 - x0 by A87, XXREAL_0:2; then A94: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6; r1 in X /\ (dom (f | X)) by A80, XBOOLE_0:def_4; then A95: (f | X) . r1 <= (f | X) . x by A63, A94, A91, RFUNCT_2:23, A88; min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17; then x0 - x < x0 - r2 by A93, XXREAL_0:2; then - (x0 - x) > - (x0 - r2) by XREAL_1:24; then A96: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6; r2 in X /\ (dom (f | X)) by A73, XBOOLE_0:def_4; then (f | X) . x <= (f | X) . r2 by A63, A96, A91, RFUNCT_2:23, A88; then A97: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A81, A74, A95; [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A79, A72, XXREAL_2:def_12; then (f | X) . x in N3 by A68, A97; hence (f | X) . x in N1 by A65; ::_thesis: verum end; supposeA98: (f | X) . x0 = p ; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 then consider r being real number such that A99: r > 0 and A100: N1 = ].(p - r),(p + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; set R = r / 2; A101: p - (r / 2) < p by A99, XREAL_1:44, XREAL_1:215; A102: p < p + (r / 2) by A99, XREAL_1:29, XREAL_1:215; then p + (r / 2) in { s where s is Real : p < s } ; then p + (r / 2) in right_open_halfline p by XXREAL_1:230; then consider r1 being Real such that A103: ( r1 in dom (f | X) & r1 in X ) and A104: p + (r / 2) = (f | X) . r1 by A3, A5, A6, PARTFUN2:59; A105: now__::_thesis:_not_x0_<_r1 assume A106: x0 < r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A103, XBOOLE_0:def_4; hence contradiction by A63, A98, A102, A104, A106, RFUNCT_2:23, A4; ::_thesis: verum end; r1 <> x0 by A98, A99, A104, XREAL_1:29, XREAL_1:215; then r1 < x0 by A105, 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 = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) assume that A107: x in dom (f | X) and A108: x in N ; ::_thesis: (f | X) . x in N1 A109: ex s being Real st ( s = x & x0 - (x0 - r1) < s & s < x0 + (x0 - r1) ) by A108; (f | X) . x in right_closed_halfline p by A3, A5, A107, FUNCT_1:def_6; then (f | X) . x in { s where s is Real : p <= s } by XXREAL_1:232; then ex s being Real st ( s = (f | X) . x & p <= s ) ; then A110: p - (r / 2) <= (f | X) . x by A101, XXREAL_0:2; A111: r1 in X /\ (dom (f | X)) by A103, XBOOLE_0:def_4; x in X /\ (dom (f | X)) by A107, XBOOLE_0:def_4; then p + (r / 2) >= (f | X) . x by A63, A104, A111, A109, RFUNCT_2:23; then A112: (f | X) . x in [.(p - (r / 2)),(p + (r / 2)).] by A110; A113: r / 2 < r by A99, XREAL_1:216; then A114: p - r < p - (r / 2) by XREAL_1:15; p < p + r by A99, XREAL_1:29; then p - (r / 2) < p + r by A101, XXREAL_0:2; then A115: p - (r / 2) in ].(p - r),(p + r).[ by A114; A116: p + (r / 2) < p + r by A113, XREAL_1:6; p - r < p by A99, XREAL_1:44; then p - r < p + (r / 2) by A102, XXREAL_0:2; then p + (r / 2) in ].(p - r),(p + r).[ by A116; then [.(p - (r / 2)),(p + (r / 2)).] c= N1 by A100, A115, XXREAL_2:def_12; hence (f | X) . x in N1 by A112; ::_thesis: verum end; end; end; hence ex N being Neighbourhood of x0 st for r1 being real number st r1 in dom (f | X) & r1 in N holds (f | X) . r1 in N1 ; ::_thesis: verum end; end; end; hence ex N being Neighbourhood of x0 st for r1 being real number st r1 in dom (f | X) & r1 in N holds (f | X) . r1 in N1 ; ::_thesis: verum end; hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum end; hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum end; theorem Th15: :: FCONT_3:15 for X being set for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p, g being Real st f .: X = ].p,g.[ holds f | X is continuous proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & ex p, g being Real st f .: X = ].p,g.[ holds f | X is continuous let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is monotone & ex p, g being Real st f .: X = ].p,g.[ implies f | X is continuous ) assume that A1: X c= dom f and A2: f | X is monotone ; ::_thesis: ( for p, g being Real holds not f .: X = ].p,g.[ or f | X is continuous ) given p, g being Real such that A3: f .: X = ].p,g.[ ; ::_thesis: f | X is continuous set L = ].p,g.[; now__::_thesis:_f_|_X_is_continuous percases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def_5; suppose f | X is non-decreasing ; ::_thesis: f | X is continuous then A4: (f | X) | X is non-decreasing ; for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) A5: x0 in REAL by XREAL_0:def_1; A6: (f | X) .: X = f .: X by RELAT_1:129; assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 then x0 in X ; then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4; then A7: x0 in dom (f | X) by RELAT_1:61; then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6; then A8: (f | X) . x0 in ].p,g.[ by A3, RELAT_1:129; now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_ for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_ (f_|_X)_._x_in_N1 let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 consider N2 being Neighbourhood of (f | X) . x0 such that A9: N2 c= ].p,g.[ by A8, RCOMP_1:18; consider N3 being Neighbourhood of (f | X) . x0 such that A10: N3 c= N1 and A11: N3 c= N2 by RCOMP_1:17; consider r being real number such that A12: r > 0 and A13: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; 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: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A14; then ((f | X) . x0) + (r / 2) in N2 by A11, A13; then consider r2 being Real such that A18: ( r2 in dom (f | X) & r2 in X ) and A19: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A6, A9, PARTFUN2:59; A20: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A12, XREAL_1:29, XREAL_1:215; A21: now__::_thesis:_not_r2_<_x0 assume A22: r2 < x0 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A18, XBOOLE_0:def_4; hence contradiction by A4, A19, A20, A22, RFUNCT_2:22, A5; ::_thesis: verum 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: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A23; then ((f | X) . x0) - (r / 2) in N2 by A11, A13; then consider r1 being Real such that A25: ( r1 in dom (f | X) & r1 in X ) and A26: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A6, A9, PARTFUN2:59; A27: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A12, XREAL_1:29, XREAL_1:215; then A28: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19; A29: now__::_thesis:_not_x0_<_r1 assume A30: x0 < r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A25, XBOOLE_0:def_4; hence contradiction by A4, A26, A28, A30, RFUNCT_2:22, A5; ::_thesis: verum 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: min ((x0 - r1),(r2 - x0)) <= 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 min ((x0 - r1),(r2 - x0)) > 0 by A31, XXREAL_0:15; then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6; take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) A33: x in REAL by XREAL_0:def_1; assume that A34: x in dom (f | X) and A35: x in N ; ::_thesis: (f | X) . x in N1 A36: x in X /\ (dom (f | X)) by A34, XBOOLE_1:28; A37: ex s being Real st ( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A35; then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19; then A38: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9; min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17; then x0 - x < x0 - r1 by A38, XXREAL_0:2; then - (x0 - x) > - (x0 - r1) by XREAL_1:24; then A39: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6; r1 in X /\ (dom (f | X)) by A25, XBOOLE_0:def_4; then A40: (f | X) . r1 <= (f | X) . x by A4, A39, A36, RFUNCT_2:22, A33; x - x0 < min ((x0 - r1),(r2 - x0)) by A37, XREAL_1:19; then x - x0 < r2 - x0 by A32, XXREAL_0:2; then A41: (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 A4, A41, A36, RFUNCT_2:22, A33; then A42: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A26, A19, A40; [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A24, A17, XXREAL_2:def_12; then (f | X) . x in N3 by A13, A42; hence (f | X) . x in N1 by A10; ::_thesis: verum end; hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum end; hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum end; suppose f | X is non-increasing ; ::_thesis: f | X is continuous then A43: (f | X) | X is non-increasing ; for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) A44: x0 in REAL by XREAL_0:def_1; A45: (f | X) .: X = f .: X by RELAT_1:129; assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 then x0 in X ; then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4; then A46: x0 in dom (f | X) by RELAT_1:61; then (f | X) . x0 in (f | X) .: X by FUNCT_1:def_6; then A47: (f | X) . x0 in ].p,g.[ by A3, RELAT_1:129; now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_ for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_ (f_|_X)_._x_in_N1 let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 consider N2 being Neighbourhood of (f | X) . x0 such that A48: N2 c= ].p,g.[ by A47, RCOMP_1:18; consider N3 being Neighbourhood of (f | X) . x0 such that A49: N3 c= N1 and A50: N3 c= N2 by RCOMP_1:17; consider r being real number such that A51: r > 0 and A52: N3 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; A53: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A51, XREAL_1:29, XREAL_1:215; set M2 = ((f | X) . x0) + (r / 2); A54: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A51, XREAL_1:29, XREAL_1:215; A55: (f | X) . x0 < ((f | X) . x0) + r by A51, 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 A54, XXREAL_0:2; then A56: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A53; then ((f | X) . x0) + (r / 2) in N2 by A50, A52; then consider r2 being Real such that A57: ( r2 in dom (f | X) & r2 in X ) and A58: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A45, A48, PARTFUN2:59; A59: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A51, XREAL_1:29, XREAL_1:215; A60: now__::_thesis:_not_r2_>_x0 assume A61: r2 > x0 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A46, A57, XBOOLE_0:def_4; hence contradiction by A43, A58, A59, A61, RFUNCT_2:23, A44; ::_thesis: verum end; set M1 = ((f | X) . x0) - (r / 2); A62: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A51, XREAL_1:29, XREAL_1:215; ((f | X) . x0) - (r / 2) < (f | X) . x0 by A54, XREAL_1:19; then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A55, XXREAL_0:2; then A63: ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A62; then ((f | X) . x0) - (r / 2) in N2 by A50, A52; then consider r1 being Real such that A64: ( r1 in dom (f | X) & r1 in X ) and A65: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A45, A48, PARTFUN2:59; A66: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A51, XREAL_1:29, XREAL_1:215; then A67: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19; A68: now__::_thesis:_not_x0_>_r1 assume A69: x0 > r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A46, A64, XBOOLE_0:def_4; hence contradiction by A43, A65, A67, A69, RFUNCT_2:23, A44; ::_thesis: verum end; x0 <> r2 by A51, A58, XREAL_1:29, XREAL_1:215; then x0 > r2 by A60, XXREAL_0:1; then A70: x0 - r2 > 0 by XREAL_1:50; set R = min ((r1 - x0),(x0 - r2)); A71: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17; r1 <> x0 by A65, A66, XREAL_1:19; then r1 > x0 by A68, XXREAL_0:1; then r1 - x0 > 0 by XREAL_1:50; then min ((r1 - x0),(x0 - r2)) > 0 by A70, XXREAL_0:15; then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6; take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) A72: x in REAL by XREAL_0:def_1; assume that A73: x in dom (f | X) and A74: x in N ; ::_thesis: (f | X) . x in N1 A75: x in X /\ (dom (f | X)) by A73, XBOOLE_1:28; A76: ex s being Real st ( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A74; then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19; then A77: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9; x - x0 < min ((r1 - x0),(x0 - r2)) by A76, XREAL_1:19; then x - x0 < r1 - x0 by A71, XXREAL_0:2; then A78: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6; r1 in X /\ (dom (f | X)) by A64, XBOOLE_0:def_4; then A79: (f | X) . r1 <= (f | X) . x by A43, A78, A75, RFUNCT_2:23, A72; min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17; then x0 - x < x0 - r2 by A77, XXREAL_0:2; then - (x0 - x) > - (x0 - r2) by XREAL_1:24; then A80: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6; r2 in X /\ (dom (f | X)) by A57, XBOOLE_0:def_4; then (f | X) . x <= (f | X) . r2 by A43, A80, A75, RFUNCT_2:23, A72; then A81: (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A65, A58, A79; [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A63, A56, XXREAL_2:def_12; then (f | X) . x in N3 by A52, A81; hence (f | X) . x in N1 by A49; ::_thesis: verum end; hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum end; hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum end; end; end; hence f | X is continuous ; ::_thesis: verum end; theorem Th16: :: FCONT_3:16 for X being set for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & f .: X = REAL holds f | X is continuous proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is monotone & f .: X = REAL holds f | X is continuous let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is monotone & f .: X = REAL implies f | X is continuous ) assume that A1: X c= dom f and A2: f | X is monotone and A3: f .: X = REAL ; ::_thesis: f | X is continuous now__::_thesis:_f_|_X_is_continuous percases ( f | X is non-decreasing or f | X is non-increasing ) by A2, RFUNCT_2:def_5; suppose f | X is non-decreasing ; ::_thesis: f | X is continuous then A4: (f | X) | X is non-decreasing ; for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) A5: x0 in REAL by XREAL_0:def_1; A6: (f | X) .: X = f .: X by RELAT_1:129; assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 then x0 in X ; then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4; then A7: x0 in dom (f | X) by RELAT_1:61; now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_ for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_ (f_|_X)_._x_in_N1 let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 consider r being real number such that A8: r > 0 and A9: N1 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; A10: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A8, XREAL_1:29, XREAL_1:215; set M1 = ((f | X) . x0) - (r / 2); consider r1 being Real such that A11: ( r1 in dom (f | X) & r1 in X ) and A12: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A6, PARTFUN2:59; A13: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A8, XREAL_1:29, XREAL_1:215; then A14: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19; A15: now__::_thesis:_not_x0_<_r1 assume A16: x0 < r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A7, A11, XBOOLE_0:def_4; hence contradiction by A4, A12, A14, A16, RFUNCT_2:22, A5; ::_thesis: verum end; set M2 = ((f | X) . x0) + (r / 2); consider r2 being Real such that A17: ( r2 in dom (f | X) & r2 in X ) and A18: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A6, PARTFUN2:59; A19: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A8, XREAL_1:29, XREAL_1:215; A20: now__::_thesis:_not_r2_<_x0 assume A21: r2 < x0 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A7, A17, XBOOLE_0:def_4; hence contradiction by A4, A18, A19, A21, RFUNCT_2:22, A5; ::_thesis: verum end; x0 <> r2 by A8, A18, XREAL_1:29, XREAL_1:215; then x0 < r2 by A20, XXREAL_0:1; then A22: r2 - x0 > 0 by XREAL_1:50; set R = min ((x0 - r1),(r2 - x0)); A23: min ((x0 - r1),(r2 - x0)) <= r2 - x0 by XXREAL_0:17; r1 <> x0 by A12, A13, XREAL_1:19; then r1 < x0 by A15, XXREAL_0:1; then x0 - r1 > 0 by XREAL_1:50; then min ((x0 - r1),(r2 - x0)) > 0 by A22, XXREAL_0:15; then reconsider N = ].(x0 - (min ((x0 - r1),(r2 - x0)))),(x0 + (min ((x0 - r1),(r2 - x0)))).[ as Neighbourhood of x0 by RCOMP_1:def_6; take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) A24: x in REAL by XREAL_0:def_1; assume that A25: x in dom (f | X) and A26: x in N ; ::_thesis: (f | X) . x in N1 A27: x in X /\ (dom (f | X)) by A25, XBOOLE_1:28; A28: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A8, XREAL_1:29, XREAL_1:215; A29: (f | X) . x0 < ((f | X) . x0) + r by A8, 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 A10, XXREAL_0:2; then A30: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A28; A31: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A8, XREAL_1:29, XREAL_1:215; ((f | X) . x0) - (r / 2) < (f | X) . x0 by A10, XREAL_1:19; then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A29, XXREAL_0:2; then ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A31; then A32: [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A30, XXREAL_2:def_12; A33: ex s being Real st ( s = x & x0 - (min ((x0 - r1),(r2 - x0))) < s & s < x0 + (min ((x0 - r1),(r2 - x0))) ) by A26; then x0 < (min ((x0 - r1),(r2 - x0))) + x by XREAL_1:19; then A34: x0 - x < ((min ((x0 - r1),(r2 - x0))) + x) - x by XREAL_1:9; min ((x0 - r1),(r2 - x0)) <= x0 - r1 by XXREAL_0:17; then x0 - x < x0 - r1 by A34, XXREAL_0:2; then - (x0 - x) > - (x0 - r1) by XREAL_1:24; then A35: (x - x0) + x0 > (r1 - x0) + x0 by XREAL_1:6; r1 in X /\ (dom (f | X)) by A11, XBOOLE_0:def_4; then A36: (f | X) . r1 <= (f | X) . x by A4, A35, A27, RFUNCT_2:22, A24; x - x0 < min ((x0 - r1),(r2 - x0)) by A33, XREAL_1:19; then x - x0 < r2 - x0 by A23, XXREAL_0:2; then A37: (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, A37, A27, RFUNCT_2:22, A24; then (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A12, A18, A36; hence (f | X) . x in N1 by A9, A32; ::_thesis: verum end; hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum end; hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum end; suppose f | X is non-increasing ; ::_thesis: f | X is continuous then A38: (f | X) | X is non-increasing ; for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) A39: x0 in REAL by XREAL_0:def_1; A40: (f | X) .: X = f .: X by RELAT_1:129; assume x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 then x0 in X ; then x0 in (dom f) /\ X by A1, XBOOLE_0:def_4; then A41: x0 in dom (f | X) by RELAT_1:61; now__::_thesis:_for_N1_being_Neighbourhood_of_(f_|_X)_._x0_ex_N_being_Neighbourhood_of_x0_st_ for_x_being_real_number_st_x_in_dom_(f_|_X)_&_x_in_N_holds_ (f_|_X)_._x_in_N1 let N1 be Neighbourhood of (f | X) . x0; ::_thesis: ex N being Neighbourhood of x0 st for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 consider r being real number such that A42: r > 0 and A43: N1 = ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by RCOMP_1:def_6; reconsider r = r as Real by XREAL_0:def_1; A44: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A42, XREAL_1:29, XREAL_1:215; set M1 = ((f | X) . x0) - (r / 2); consider r1 being Real such that A45: ( r1 in dom (f | X) & r1 in X ) and A46: ((f | X) . x0) - (r / 2) = (f | X) . r1 by A3, A40, PARTFUN2:59; A47: (f | X) . x0 < ((f | X) . x0) + (r / 2) by A42, XREAL_1:29, XREAL_1:215; then A48: ((f | X) . x0) - (r / 2) < (f | X) . x0 by XREAL_1:19; A49: now__::_thesis:_not_x0_>_r1 assume A50: x0 > r1 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r1 in X /\ (dom (f | X)) ) by A41, A45, XBOOLE_0:def_4; hence contradiction by A38, A46, A48, A50, RFUNCT_2:23, A39; ::_thesis: verum end; set M2 = ((f | X) . x0) + (r / 2); consider r2 being Real such that A51: ( r2 in dom (f | X) & r2 in X ) and A52: ((f | X) . x0) + (r / 2) = (f | X) . r2 by A3, A40, PARTFUN2:59; A53: ((f | X) . x0) + (r / 2) > (f | X) . x0 by A42, XREAL_1:29, XREAL_1:215; A54: now__::_thesis:_not_r2_>_x0 assume A55: r2 > x0 ; ::_thesis: contradiction ( x0 in X /\ (dom (f | X)) & r2 in X /\ (dom (f | X)) ) by A41, A51, XBOOLE_0:def_4; hence contradiction by A38, A52, A53, A55, RFUNCT_2:23, A39; ::_thesis: verum end; x0 <> r2 by A42, A52, XREAL_1:29, XREAL_1:215; then x0 > r2 by A54, XXREAL_0:1; then A56: x0 - r2 > 0 by XREAL_1:50; set R = min ((r1 - x0),(x0 - r2)); A57: min ((r1 - x0),(x0 - r2)) <= r1 - x0 by XXREAL_0:17; r1 <> x0 by A46, A47, XREAL_1:19; then r1 > x0 by A49, XXREAL_0:1; then r1 - x0 > 0 by XREAL_1:50; then min ((r1 - x0),(x0 - r2)) > 0 by A56, XXREAL_0:15; then reconsider N = ].(x0 - (min ((r1 - x0),(x0 - r2)))),(x0 + (min ((r1 - x0),(x0 - r2)))).[ as Neighbourhood of x0 by RCOMP_1:def_6; take N = N; ::_thesis: for x being real number st x in dom (f | X) & x in N holds (f | X) . x in N1 let x be real number ; ::_thesis: ( x in dom (f | X) & x in N implies (f | X) . x in N1 ) A58: x in REAL by XREAL_0:def_1; assume that A59: x in dom (f | X) and A60: x in N ; ::_thesis: (f | X) . x in N1 A61: x in X /\ (dom (f | X)) by A59, XBOOLE_1:28; A62: ((f | X) . x0) + (r / 2) < (((f | X) . x0) + (r / 2)) + (r / 2) by A42, XREAL_1:29, XREAL_1:215; A63: (f | X) . x0 < ((f | X) . x0) + r by A42, 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 A44, XXREAL_0:2; then A64: ((f | X) . x0) + (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A62; A65: ((f | X) . x0) - r < (((f | X) . x0) - r) + (r / 2) by A42, XREAL_1:29, XREAL_1:215; ((f | X) . x0) - (r / 2) < (f | X) . x0 by A44, XREAL_1:19; then ((f | X) . x0) - (r / 2) < ((f | X) . x0) + r by A63, XXREAL_0:2; then ((f | X) . x0) - (r / 2) in ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A65; then A66: [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] c= ].(((f | X) . x0) - r),(((f | X) . x0) + r).[ by A64, XXREAL_2:def_12; A67: ex s being Real st ( s = x & x0 - (min ((r1 - x0),(x0 - r2))) < s & s < x0 + (min ((r1 - x0),(x0 - r2))) ) by A60; then x0 < (min ((r1 - x0),(x0 - r2))) + x by XREAL_1:19; then A68: x0 - x < ((min ((r1 - x0),(x0 - r2))) + x) - x by XREAL_1:9; x - x0 < min ((r1 - x0),(x0 - r2)) by A67, XREAL_1:19; then x - x0 < r1 - x0 by A57, XXREAL_0:2; then A69: (x - x0) + x0 < (r1 - x0) + x0 by XREAL_1:6; r1 in X /\ (dom (f | X)) by A45, XBOOLE_0:def_4; then A70: (f | X) . r1 <= (f | X) . x by A38, A69, A61, RFUNCT_2:23, A58; min ((r1 - x0),(x0 - r2)) <= x0 - r2 by XXREAL_0:17; then x0 - x < x0 - r2 by A68, XXREAL_0:2; then - (x0 - x) > - (x0 - r2) by XREAL_1:24; then A71: (x - x0) + x0 > (r2 - x0) + x0 by XREAL_1:6; r2 in X /\ (dom (f | X)) by A51, XBOOLE_0:def_4; then (f | X) . x <= (f | X) . r2 by A38, A71, A61, RFUNCT_2:23, A58; then (f | X) . x in [.(((f | X) . x0) - (r / 2)),(((f | X) . x0) + (r / 2)).] by A46, A52, A70; hence (f | X) . x in N1 by A43, A66; ::_thesis: verum end; hence f | X is_continuous_in x0 by FCONT_1:4; ::_thesis: verum end; hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum end; end; end; hence f | X is continuous ; ::_thesis: verum end; theorem :: FCONT_3:17 for p, g being Real for f being 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 p, g be Real; ::_thesis: for f being 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 let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) & ].p,g.[ c= dom f implies ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous ) assume that A1: ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) and A2: ].p,g.[ c= dom f ; ::_thesis: ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous now__::_thesis:_((f_|_].p,g.[)_")_|_(f_.:_].p,g.[)_is_continuous percases ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) by A1; supposeA3: f | ].p,g.[ is increasing ; ::_thesis: ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous A4: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_].p,g.[_holds_ r_in_dom_((f_|_].p,g.[)_") let r be Real; ::_thesis: ( r in f .: ].p,g.[ implies r in dom ((f | ].p,g.[) ") ) assume r in f .: ].p,g.[ ; ::_thesis: r in dom ((f | ].p,g.[) ") then consider s being 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; ::_thesis: verum 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 ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous by A4, A8, Th15, SUBSET_1:2; ::_thesis: verum end; supposeA9: f | ].p,g.[ is decreasing ; ::_thesis: ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous A10: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_].p,g.[_holds_ r_in_dom_((f_|_].p,g.[)_") let r be Real; ::_thesis: ( r in f .: ].p,g.[ implies r in dom ((f | ].p,g.[) ") ) assume r in f .: ].p,g.[ ; ::_thesis: r in dom ((f | ].p,g.[) ") then consider s being 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; ::_thesis: verum 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 ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous by A10, A14, Th15, SUBSET_1:2; ::_thesis: verum end; end; end; hence ((f | ].p,g.[) ") | (f .: ].p,g.[) is continuous ; ::_thesis: verum end; theorem :: FCONT_3:18 for p being Real for f being 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 p be Real; ::_thesis: for f being 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 let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) & left_open_halfline p c= dom f implies ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous ) set L = left_open_halfline p; assume that A1: ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) and A2: left_open_halfline p c= dom f ; ::_thesis: ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous now__::_thesis:_((f_|_(left_open_halfline_p))_")_|_(f_.:_(left_open_halfline_p))_is_continuous percases ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) by A1; supposeA3: f | (left_open_halfline p) is increasing ; ::_thesis: ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous A4: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(left_open_halfline_p)_holds_ r_in_dom_((f_|_(left_open_halfline_p))_") let r be Real; ::_thesis: ( r in f .: (left_open_halfline p) implies r in dom ((f | (left_open_halfline p)) ") ) assume r in f .: (left_open_halfline p) ; ::_thesis: r in dom ((f | (left_open_halfline p)) ") then consider s being Real such that A5: ( s in dom f & s in left_open_halfline p ) and A6: r = f . s by PARTFUN2:59; s in (dom f) /\ (left_open_halfline p) by A5, XBOOLE_0:def_4; then A7: s in dom (f | (left_open_halfline p)) by RELAT_1:61; then r = (f | (left_open_halfline p)) . s by A6, FUNCT_1:47; then r in rng (f | (left_open_halfline p)) by A7, FUNCT_1:def_3; hence r in dom ((f | (left_open_halfline p)) ") by FUNCT_1:33; ::_thesis: verum end; A8: ((f | (left_open_halfline p)) ") .: (f .: (left_open_halfline p)) = ((f | (left_open_halfline p)) ") .: (rng (f | (left_open_halfline p))) by RELAT_1:115 .= ((f | (left_open_halfline p)) ") .: (dom ((f | (left_open_halfline p)) ")) by FUNCT_1:33 .= rng ((f | (left_open_halfline p)) ") by RELAT_1:113 .= dom (f | (left_open_halfline p)) by FUNCT_1:33 .= (dom f) /\ (left_open_halfline p) by RELAT_1:61 .= left_open_halfline p by A2, XBOOLE_1:28 ; ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is increasing by A3, Th9; hence ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous by A4, A8, Th11, SUBSET_1:2; ::_thesis: verum end; supposeA9: f | (left_open_halfline p) is decreasing ; ::_thesis: ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous A10: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(left_open_halfline_p)_holds_ r_in_dom_((f_|_(left_open_halfline_p))_") let r be Real; ::_thesis: ( r in f .: (left_open_halfline p) implies r in dom ((f | (left_open_halfline p)) ") ) assume r in f .: (left_open_halfline p) ; ::_thesis: r in dom ((f | (left_open_halfline p)) ") then consider s being Real such that A11: ( s in dom f & s in left_open_halfline p ) and A12: r = f . s by PARTFUN2:59; s in (dom f) /\ (left_open_halfline p) by A11, XBOOLE_0:def_4; then A13: s in dom (f | (left_open_halfline p)) by RELAT_1:61; then r = (f | (left_open_halfline p)) . s by A12, FUNCT_1:47; then r in rng (f | (left_open_halfline p)) by A13, FUNCT_1:def_3; hence r in dom ((f | (left_open_halfline p)) ") by FUNCT_1:33; ::_thesis: verum end; A14: ((f | (left_open_halfline p)) ") .: (f .: (left_open_halfline p)) = ((f | (left_open_halfline p)) ") .: (rng (f | (left_open_halfline p))) by RELAT_1:115 .= ((f | (left_open_halfline p)) ") .: (dom ((f | (left_open_halfline p)) ")) by FUNCT_1:33 .= rng ((f | (left_open_halfline p)) ") by RELAT_1:113 .= dom (f | (left_open_halfline p)) by FUNCT_1:33 .= (dom f) /\ (left_open_halfline p) by RELAT_1:61 .= left_open_halfline p by A2, XBOOLE_1:28 ; ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is decreasing by A9, Th10; hence ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous by A10, A14, Th11, SUBSET_1:2; ::_thesis: verum end; end; end; hence ((f | (left_open_halfline p)) ") | (f .: (left_open_halfline p)) is continuous ; ::_thesis: verum end; theorem :: FCONT_3:19 for p being Real for f being 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 p be Real; ::_thesis: for f being 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 let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) & right_open_halfline p c= dom f implies ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous ) set L = right_open_halfline p; assume that A1: ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) and A2: right_open_halfline p c= dom f ; ::_thesis: ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous now__::_thesis:_((f_|_(right_open_halfline_p))_")_|_(f_.:_(right_open_halfline_p))_is_continuous percases ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) by A1; supposeA3: f | (right_open_halfline p) is increasing ; ::_thesis: ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous A4: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(right_open_halfline_p)_holds_ r_in_dom_((f_|_(right_open_halfline_p))_") let r be Real; ::_thesis: ( r in f .: (right_open_halfline p) implies r in dom ((f | (right_open_halfline p)) ") ) assume r in f .: (right_open_halfline p) ; ::_thesis: r in dom ((f | (right_open_halfline p)) ") then consider s being Real such that A5: ( s in dom f & s in right_open_halfline p ) and A6: r = f . s by PARTFUN2:59; s in (dom f) /\ (right_open_halfline p) by A5, XBOOLE_0:def_4; then A7: s in dom (f | (right_open_halfline p)) by RELAT_1:61; then r = (f | (right_open_halfline p)) . s by A6, FUNCT_1:47; then r in rng (f | (right_open_halfline p)) by A7, FUNCT_1:def_3; hence r in dom ((f | (right_open_halfline p)) ") by FUNCT_1:33; ::_thesis: verum end; A8: ((f | (right_open_halfline p)) ") .: (f .: (right_open_halfline p)) = ((f | (right_open_halfline p)) ") .: (rng (f | (right_open_halfline p))) by RELAT_1:115 .= ((f | (right_open_halfline p)) ") .: (dom ((f | (right_open_halfline p)) ")) by FUNCT_1:33 .= rng ((f | (right_open_halfline p)) ") by RELAT_1:113 .= dom (f | (right_open_halfline p)) by FUNCT_1:33 .= (dom f) /\ (right_open_halfline p) by RELAT_1:61 .= right_open_halfline p by A2, XBOOLE_1:28 ; ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is increasing by A3, Th9; hence ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous by A4, A8, Th12, SUBSET_1:2; ::_thesis: verum end; supposeA9: f | (right_open_halfline p) is decreasing ; ::_thesis: ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous A10: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(right_open_halfline_p)_holds_ r_in_dom_((f_|_(right_open_halfline_p))_") let r be Real; ::_thesis: ( r in f .: (right_open_halfline p) implies r in dom ((f | (right_open_halfline p)) ") ) assume r in f .: (right_open_halfline p) ; ::_thesis: r in dom ((f | (right_open_halfline p)) ") then consider s being Real such that A11: ( s in dom f & s in right_open_halfline p ) and A12: r = f . s by PARTFUN2:59; s in (dom f) /\ (right_open_halfline p) by A11, XBOOLE_0:def_4; then A13: s in dom (f | (right_open_halfline p)) by RELAT_1:61; then r = (f | (right_open_halfline p)) . s by A12, FUNCT_1:47; then r in rng (f | (right_open_halfline p)) by A13, FUNCT_1:def_3; hence r in dom ((f | (right_open_halfline p)) ") by FUNCT_1:33; ::_thesis: verum end; A14: ((f | (right_open_halfline p)) ") .: (f .: (right_open_halfline p)) = ((f | (right_open_halfline p)) ") .: (rng (f | (right_open_halfline p))) by RELAT_1:115 .= ((f | (right_open_halfline p)) ") .: (dom ((f | (right_open_halfline p)) ")) by FUNCT_1:33 .= rng ((f | (right_open_halfline p)) ") by RELAT_1:113 .= dom (f | (right_open_halfline p)) by FUNCT_1:33 .= (dom f) /\ (right_open_halfline p) by RELAT_1:61 .= right_open_halfline p by A2, XBOOLE_1:28 ; ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is decreasing by A9, Th10; hence ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous by A10, A14, Th12, SUBSET_1:2; ::_thesis: verum end; end; end; hence ((f | (right_open_halfline p)) ") | (f .: (right_open_halfline p)) is continuous ; ::_thesis: verum end; theorem :: FCONT_3:20 for p being Real for f being 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 p be Real; ::_thesis: for f being 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 let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( ( f | (left_closed_halfline p) is increasing or f | (left_closed_halfline p) is decreasing ) & left_closed_halfline p c= dom f implies ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous ) set L = left_closed_halfline p; assume that A1: ( f | (left_closed_halfline p) is increasing or f | (left_closed_halfline p) is decreasing ) and A2: left_closed_halfline p c= dom f ; ::_thesis: ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous now__::_thesis:_((f_|_(left_closed_halfline_p))_")_|_(f_.:_(left_closed_halfline_p))_is_continuous percases ( f | (left_closed_halfline p) is increasing or f | (left_closed_halfline p) is decreasing ) by A1; supposeA3: f | (left_closed_halfline p) is increasing ; ::_thesis: ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous A4: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(left_closed_halfline_p)_holds_ r_in_dom_((f_|_(left_closed_halfline_p))_") let r be Real; ::_thesis: ( r in f .: (left_closed_halfline p) implies r in dom ((f | (left_closed_halfline p)) ") ) assume r in f .: (left_closed_halfline p) ; ::_thesis: r in dom ((f | (left_closed_halfline p)) ") then consider s being Real such that A5: ( s in dom f & s in left_closed_halfline p ) and A6: r = f . s by PARTFUN2:59; s in (dom f) /\ (left_closed_halfline p) by A5, XBOOLE_0:def_4; then A7: s in dom (f | (left_closed_halfline p)) by RELAT_1:61; then r = (f | (left_closed_halfline p)) . s by A6, FUNCT_1:47; then r in rng (f | (left_closed_halfline p)) by A7, FUNCT_1:def_3; hence r in dom ((f | (left_closed_halfline p)) ") by FUNCT_1:33; ::_thesis: verum end; A8: ((f | (left_closed_halfline p)) ") .: (f .: (left_closed_halfline p)) = ((f | (left_closed_halfline p)) ") .: (rng (f | (left_closed_halfline p))) by RELAT_1:115 .= ((f | (left_closed_halfline p)) ") .: (dom ((f | (left_closed_halfline p)) ")) by FUNCT_1:33 .= rng ((f | (left_closed_halfline p)) ") by RELAT_1:113 .= dom (f | (left_closed_halfline p)) by FUNCT_1:33 .= (dom f) /\ (left_closed_halfline p) by RELAT_1:61 .= left_closed_halfline p by A2, XBOOLE_1:28 ; ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is increasing by A3, Th9; hence ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous by A4, A8, Th13, SUBSET_1:2; ::_thesis: verum end; supposeA9: f | (left_closed_halfline p) is decreasing ; ::_thesis: ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous A10: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(left_closed_halfline_p)_holds_ r_in_dom_((f_|_(left_closed_halfline_p))_") let r be Real; ::_thesis: ( r in f .: (left_closed_halfline p) implies r in dom ((f | (left_closed_halfline p)) ") ) assume r in f .: (left_closed_halfline p) ; ::_thesis: r in dom ((f | (left_closed_halfline p)) ") then consider s being Real such that A11: ( s in dom f & s in left_closed_halfline p ) and A12: r = f . s by PARTFUN2:59; s in (dom f) /\ (left_closed_halfline p) by A11, XBOOLE_0:def_4; then A13: s in dom (f | (left_closed_halfline p)) by RELAT_1:61; then r = (f | (left_closed_halfline p)) . s by A12, FUNCT_1:47; then r in rng (f | (left_closed_halfline p)) by A13, FUNCT_1:def_3; hence r in dom ((f | (left_closed_halfline p)) ") by FUNCT_1:33; ::_thesis: verum end; A14: ((f | (left_closed_halfline p)) ") .: (f .: (left_closed_halfline p)) = ((f | (left_closed_halfline p)) ") .: (rng (f | (left_closed_halfline p))) by RELAT_1:115 .= ((f | (left_closed_halfline p)) ") .: (dom ((f | (left_closed_halfline p)) ")) by FUNCT_1:33 .= rng ((f | (left_closed_halfline p)) ") by RELAT_1:113 .= dom (f | (left_closed_halfline p)) by FUNCT_1:33 .= (dom f) /\ (left_closed_halfline p) by RELAT_1:61 .= left_closed_halfline p by A2, XBOOLE_1:28 ; ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is decreasing by A9, Th10; hence ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous by A10, A14, Th13, SUBSET_1:2; ::_thesis: verum end; end; end; hence ((f | (left_closed_halfline p)) ") | (f .: (left_closed_halfline p)) is continuous ; ::_thesis: verum end; theorem :: FCONT_3:21 for p being Real for f being 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 p be Real; ::_thesis: for f being 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 let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( ( f | (right_closed_halfline p) is increasing or f | (right_closed_halfline p) is decreasing ) & right_closed_halfline p c= dom f implies ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous ) set L = right_closed_halfline p; assume that A1: ( f | (right_closed_halfline p) is increasing or f | (right_closed_halfline p) is decreasing ) and A2: right_closed_halfline p c= dom f ; ::_thesis: ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous now__::_thesis:_((f_|_(right_closed_halfline_p))_")_|_(f_.:_(right_closed_halfline_p))_is_continuous percases ( f | (right_closed_halfline p) is increasing or f | (right_closed_halfline p) is decreasing ) by A1; supposeA3: f | (right_closed_halfline p) is increasing ; ::_thesis: ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous A4: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(right_closed_halfline_p)_holds_ r_in_dom_((f_|_(right_closed_halfline_p))_") let r be Real; ::_thesis: ( r in f .: (right_closed_halfline p) implies r in dom ((f | (right_closed_halfline p)) ") ) assume r in f .: (right_closed_halfline p) ; ::_thesis: r in dom ((f | (right_closed_halfline p)) ") then consider s being Real such that A5: ( s in dom f & s in right_closed_halfline p ) and A6: r = f . s by PARTFUN2:59; s in (dom f) /\ (right_closed_halfline p) by A5, XBOOLE_0:def_4; then A7: s in dom (f | (right_closed_halfline p)) by RELAT_1:61; then r = (f | (right_closed_halfline p)) . s by A6, FUNCT_1:47; then r in rng (f | (right_closed_halfline p)) by A7, FUNCT_1:def_3; hence r in dom ((f | (right_closed_halfline p)) ") by FUNCT_1:33; ::_thesis: verum end; A8: ((f | (right_closed_halfline p)) ") .: (f .: (right_closed_halfline p)) = ((f | (right_closed_halfline p)) ") .: (rng (f | (right_closed_halfline p))) by RELAT_1:115 .= ((f | (right_closed_halfline p)) ") .: (dom ((f | (right_closed_halfline p)) ")) by FUNCT_1:33 .= rng ((f | (right_closed_halfline p)) ") by RELAT_1:113 .= dom (f | (right_closed_halfline p)) by FUNCT_1:33 .= (dom f) /\ (right_closed_halfline p) by RELAT_1:61 .= right_closed_halfline p by A2, XBOOLE_1:28 ; ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is increasing by A3, Th9; hence ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous by A4, A8, Th14, SUBSET_1:2; ::_thesis: verum end; supposeA9: f | (right_closed_halfline p) is decreasing ; ::_thesis: ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous A10: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_(right_closed_halfline_p)_holds_ r_in_dom_((f_|_(right_closed_halfline_p))_") let r be Real; ::_thesis: ( r in f .: (right_closed_halfline p) implies r in dom ((f | (right_closed_halfline p)) ") ) assume r in f .: (right_closed_halfline p) ; ::_thesis: r in dom ((f | (right_closed_halfline p)) ") then consider s being Real such that A11: ( s in dom f & s in right_closed_halfline p ) and A12: r = f . s by PARTFUN2:59; s in (dom f) /\ (right_closed_halfline p) by A11, XBOOLE_0:def_4; then A13: s in dom (f | (right_closed_halfline p)) by RELAT_1:61; then r = (f | (right_closed_halfline p)) . s by A12, FUNCT_1:47; then r in rng (f | (right_closed_halfline p)) by A13, FUNCT_1:def_3; hence r in dom ((f | (right_closed_halfline p)) ") by FUNCT_1:33; ::_thesis: verum end; A14: ((f | (right_closed_halfline p)) ") .: (f .: (right_closed_halfline p)) = ((f | (right_closed_halfline p)) ") .: (rng (f | (right_closed_halfline p))) by RELAT_1:115 .= ((f | (right_closed_halfline p)) ") .: (dom ((f | (right_closed_halfline p)) ")) by FUNCT_1:33 .= rng ((f | (right_closed_halfline p)) ") by RELAT_1:113 .= dom (f | (right_closed_halfline p)) by FUNCT_1:33 .= (dom f) /\ (right_closed_halfline p) by RELAT_1:61 .= right_closed_halfline p by A2, XBOOLE_1:28 ; ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is decreasing by A9, Th10; hence ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous by A10, A14, Th14, SUBSET_1:2; ::_thesis: verum end; end; end; hence ((f | (right_closed_halfline p)) ") | (f .: (right_closed_halfline p)) is continuous ; ::_thesis: verum end; theorem :: FCONT_3:22 for f being 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; ::_thesis: ( ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) & f is total implies (f ") | (rng f) is continuous ) assume that A1: ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) and A2: f is total ; ::_thesis: (f ") | (rng f) is continuous A3: dom f = [#] REAL by A2, PARTFUN1:def_2; now__::_thesis:_(f_")_|_(rng_f)_is_continuous percases ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) by A1; supposeA4: f | ([#] REAL) is increasing ; ::_thesis: (f ") | (rng f) is continuous A5: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_([#]_REAL)_holds_ r_in_dom_((f_|_([#]_REAL))_") let r be Real; ::_thesis: ( r in f .: ([#] REAL) implies r in dom ((f | ([#] REAL)) ") ) assume r in f .: ([#] REAL) ; ::_thesis: r in dom ((f | ([#] REAL)) ") then consider s being Real such that A6: s in dom f and s in [#] REAL and A7: r = f . s by PARTFUN2:59; s in (dom f) /\ ([#] REAL) by A6, XBOOLE_0:def_4; then A8: s in dom (f | ([#] REAL)) by RELAT_1:61; then r = (f | ([#] REAL)) . s by A7, FUNCT_1:47; then r in rng (f | ([#] REAL)) by A8, FUNCT_1:def_3; hence r in dom ((f | ([#] REAL)) ") by FUNCT_1:33; ::_thesis: verum end; A9: ((f | ([#] REAL)) ") .: (f .: ([#] REAL)) = ((f | ([#] REAL)) ") .: (rng (f | ([#] REAL))) by RELAT_1:115 .= ((f | ([#] REAL)) ") .: (dom ((f | ([#] REAL)) ")) by FUNCT_1:33 .= rng ((f | ([#] REAL)) ") by RELAT_1:113 .= dom (f | ([#] REAL)) by FUNCT_1:33 .= (dom f) /\ ([#] REAL) by RELAT_1:61 .= REAL by A3 ; ((f | ([#] REAL)) ") | (f .: ([#] REAL)) is increasing by A4, Th9; then ((f | ([#] REAL)) ") | (f .: ([#] REAL)) is continuous by A5, A9, Th16, SUBSET_1:2; then ((f | ([#] REAL)) ") | (rng f) is continuous by A3, RELAT_1:113; hence (f ") | (rng f) is continuous by A3, RELAT_1:68; ::_thesis: verum end; supposeA10: f | ([#] REAL) is decreasing ; ::_thesis: (f ") | (rng f) is continuous A11: now__::_thesis:_for_r_being_Real_st_r_in_f_.:_([#]_REAL)_holds_ r_in_dom_((f_|_([#]_REAL))_") let r be Real; ::_thesis: ( r in f .: ([#] REAL) implies r in dom ((f | ([#] REAL)) ") ) assume r in f .: ([#] REAL) ; ::_thesis: r in dom ((f | ([#] REAL)) ") then consider s being Real such that A12: s in dom f and s in [#] REAL and A13: r = f . s by PARTFUN2:59; s in (dom f) /\ ([#] REAL) by A12, XBOOLE_0:def_4; then A14: s in dom (f | ([#] REAL)) by RELAT_1:61; then r = (f | ([#] REAL)) . s by A13, FUNCT_1:47; then r in rng (f | ([#] REAL)) by A14, FUNCT_1:def_3; hence r in dom ((f | ([#] REAL)) ") by FUNCT_1:33; ::_thesis: verum end; A15: ((f | ([#] REAL)) ") .: (f .: ([#] REAL)) = ((f | ([#] REAL)) ") .: (rng (f | ([#] REAL))) by RELAT_1:115 .= ((f | ([#] REAL)) ") .: (dom ((f | ([#] REAL)) ")) by FUNCT_1:33 .= rng ((f | ([#] REAL)) ") by RELAT_1:113 .= dom (f | ([#] REAL)) by FUNCT_1:33 .= (dom f) /\ ([#] REAL) by RELAT_1:61 .= REAL by A3 ; ((f | ([#] REAL)) ") | (f .: ([#] REAL)) is decreasing by A10, Th10; then ((f | ([#] REAL)) ") | (f .: ([#] REAL)) is continuous by A11, A15, Th16, SUBSET_1:2; then ((f | ([#] REAL)) ") | (rng f) is continuous by A3, RELAT_1:113; hence (f ") | (rng f) is continuous by A3, RELAT_1:68; ::_thesis: verum end; end; end; hence (f ") | (rng f) is continuous ; ::_thesis: verum end; theorem :: FCONT_3:23 for p, g being Real for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f | ].p,g.[ is continuous & ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) holds rng (f | ].p,g.[) is open proof let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f | ].p,g.[ is continuous & ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) holds rng (f | ].p,g.[) is open let f be PartFunc of REAL,REAL; ::_thesis: ( ].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 ) 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 ) ; ::_thesis: rng (f | ].p,g.[) is open now__::_thesis:_for_r1_being_real_number_st_r1_in_rng_(f_|_].p,g.[)_holds_ ex_N_being_Neighbourhood_of_r1_st_N_c=_rng_(f_|_].p,g.[) let r1 be real number ; ::_thesis: ( r1 in rng (f | ].p,g.[) implies ex N being Neighbourhood of r1 st N c= rng (f | ].p,g.[) ) set f1 = f | ].p,g.[; assume r1 in rng (f | ].p,g.[) ; ::_thesis: ex N being Neighbourhood of r1 st N c= rng (f | ].p,g.[) then consider x0 being Real such that A4: x0 in dom (f | ].p,g.[) and A5: (f | ].p,g.[) . 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 being Neighbourhood of x0 such that A8: N c= ].p,g.[ by RCOMP_1:18; consider r being real number such that A9: 0 < r and A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6; reconsider r = r as 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, XBOOLE_1:1; 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__::_thesis:_ex_N1_being_Neighbourhood_of_r1_st_N1_c=_rng_(f_|_].p,g.[) percases ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) by A3; supposeA25: f | ].p,g.[ is increasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | ].p,g.[) set R = min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))); f . x0 < f . (x0 + (r / 2)) by A7, A16, A21, A25, RFUNCT_2:20; then A26: 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:50; f . (x0 - (r / 2)) < f . x0 by A7, A11, A19, A25, RFUNCT_2:20; then 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:50; then 0 < min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by A26, XXREAL_0:15; then reconsider N1 = ].(r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))),(r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))).[ as Neighbourhood of r1 by RCOMP_1:def_6; take N1 = N1; ::_thesis: N1 c= rng (f | ].p,g.[) f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by A17, A21, A19, A25, RFUNCT_2:20; then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29; then A27: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ; thus N1 c= rng (f | ].p,g.[) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng (f | ].p,g.[) ) A28: ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] by XXREAL_1:25; assume x in N1 ; ::_thesis: x in rng (f | ].p,g.[) then consider r2 being Real such that A29: r2 = x and A30: (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) < r2 and A31: r2 < (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by A6; min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . (x0 + (r / 2))) - (f . x0) by XXREAL_0:17; then (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by XREAL_1:7; then A32: r2 < f . (x0 + (r / 2)) by A31, XXREAL_0:2; min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) - (f . (x0 - (r / 2))) by XXREAL_0:17; then (f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) <= (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by XREAL_1:13; then f . (x0 - (r / 2)) < r2 by A30, XXREAL_0:2; then r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A32; then consider s being Real 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 (f | ].p,g.[) by RELAT_1:61; then x = (f | ].p,g.[) . s by A34, FUNCT_1:47; hence x in rng (f | ].p,g.[) by A35, FUNCT_1:def_3; ::_thesis: verum end; end; supposeA36: f | ].p,g.[ is decreasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | ].p,g.[) set R = min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))); f . (x0 + (r / 2)) < f . x0 by A7, A16, A21, A36, RFUNCT_2:21; then A37: 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:50; f . x0 < f . (x0 - (r / 2)) by A7, A11, A19, A36, RFUNCT_2:21; then 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:50; then 0 < min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by A37, XXREAL_0:15; then reconsider N1 = ].(r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))),(r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))).[ as Neighbourhood of r1 by RCOMP_1:def_6; take N1 = N1; ::_thesis: N1 c= rng (f | ].p,g.[) f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by A17, A21, A19, A36, RFUNCT_2:21; then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29; then A38: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ; thus N1 c= rng (f | ].p,g.[) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng (f | ].p,g.[) ) A39: ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25; assume x in N1 ; ::_thesis: x in rng (f | ].p,g.[) then consider r2 being Real such that A40: r2 = x and A41: (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) < r2 and A42: r2 < (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by A6; min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . (x0 - (r / 2))) - (f . x0) by XXREAL_0:17; then (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by XREAL_1:7; then A43: r2 < f . (x0 - (r / 2)) by A42, XXREAL_0:2; min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . x0) - (f . (x0 + (r / 2))) by XXREAL_0:17; then (f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by XREAL_1:13; then f . (x0 + (r / 2)) < r2 by A41, XXREAL_0:2; then r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A43; then consider s being Real 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 (f | ].p,g.[) by RELAT_1:61; then x = (f | ].p,g.[) . s by A45, FUNCT_1:47; hence x in rng (f | ].p,g.[) by A46, FUNCT_1:def_3; ::_thesis: verum end; end; end; end; hence ex N being Neighbourhood of r1 st N c= rng (f | ].p,g.[) ; ::_thesis: verum end; hence rng (f | ].p,g.[) is open by RCOMP_1:20; ::_thesis: verum end; theorem :: FCONT_3:24 for p being Real for f being PartFunc of REAL,REAL st 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 ) holds rng (f | (left_open_halfline p)) is open proof let p be Real; ::_thesis: for f being PartFunc of REAL,REAL st 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 ) holds rng (f | (left_open_halfline p)) is open let f be PartFunc of REAL,REAL; ::_thesis: ( 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 ) set L = left_open_halfline p; assume that A1: left_open_halfline p c= dom f and A2: f | (left_open_halfline p) is continuous and A3: ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) ; ::_thesis: rng (f | (left_open_halfline p)) is open now__::_thesis:_for_r1_being_real_number_st_r1_in_rng_(f_|_(left_open_halfline_p))_holds_ ex_N_being_Neighbourhood_of_r1_st_N_c=_rng_(f_|_(left_open_halfline_p)) let r1 be real number ; ::_thesis: ( r1 in rng (f | (left_open_halfline p)) implies ex N being Neighbourhood of r1 st N c= rng (f | (left_open_halfline p)) ) set f1 = f | (left_open_halfline p); assume r1 in rng (f | (left_open_halfline p)) ; ::_thesis: ex N being Neighbourhood of r1 st N c= rng (f | (left_open_halfline p)) then consider x0 being Real such that A4: x0 in dom (f | (left_open_halfline p)) and A5: (f | (left_open_halfline p)) . x0 = r1 by PARTFUN1:3; A6: r1 = f . x0 by A4, A5, FUNCT_1:47; A7: x0 in (dom f) /\ (left_open_halfline p) by A4, RELAT_1:61; then x0 in left_open_halfline p by XBOOLE_0:def_4; then consider N being Neighbourhood of x0 such that A8: N c= left_open_halfline p by RCOMP_1:18; consider r being real number such that A9: 0 < r and A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6; reconsider r = r as 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, XBOOLE_1:1; 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 (left_open_halfline p) /\ (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 (left_open_halfline p) /\ (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= left_open_halfline p by A8, A10, A18, A20, XXREAL_2:def_12; now__::_thesis:_ex_N1_being_Neighbourhood_of_r1_st_N1_c=_rng_(f_|_(left_open_halfline_p)) percases ( f | (left_open_halfline p) is increasing or f | (left_open_halfline p) is decreasing ) by A3; supposeA25: f | (left_open_halfline p) is increasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | (left_open_halfline p)) set R = min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))); f . x0 < f . (x0 + (r / 2)) by A7, A16, A21, A25, RFUNCT_2:20; then A26: 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:50; f . (x0 - (r / 2)) < f . x0 by A7, A11, A19, A25, RFUNCT_2:20; then 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:50; then 0 < min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by A26, XXREAL_0:15; then reconsider N1 = ].(r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))),(r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))).[ as Neighbourhood of r1 by RCOMP_1:def_6; take N1 = N1; ::_thesis: N1 c= rng (f | (left_open_halfline p)) f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by A17, A21, A19, A25, RFUNCT_2:20; then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29; then A27: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ; thus N1 c= rng (f | (left_open_halfline p)) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng (f | (left_open_halfline p)) ) A28: ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] by XXREAL_1:25; assume x in N1 ; ::_thesis: x in rng (f | (left_open_halfline p)) then consider r2 being Real such that A29: r2 = x and A30: (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) < r2 and A31: r2 < (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by A6; min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . (x0 + (r / 2))) - (f . x0) by XXREAL_0:17; then (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by XREAL_1:7; then A32: r2 < f . (x0 + (r / 2)) by A31, XXREAL_0:2; min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) - (f . (x0 - (r / 2))) by XXREAL_0:17; then (f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) <= (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by XREAL_1:13; then f . (x0 - (r / 2)) < r2 by A30, XXREAL_0:2; then r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A32; then consider s being Real 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) /\ (left_open_halfline p) by A8, A14, XBOOLE_0:def_4; then A35: s in dom (f | (left_open_halfline p)) by RELAT_1:61; then x = (f | (left_open_halfline p)) . s by A34, FUNCT_1:47; hence x in rng (f | (left_open_halfline p)) by A35, FUNCT_1:def_3; ::_thesis: verum end; end; supposeA36: f | (left_open_halfline p) is decreasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | (left_open_halfline p)) set R = min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))); f . (x0 + (r / 2)) < f . x0 by A7, A16, A21, A36, RFUNCT_2:21; then A37: 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:50; f . x0 < f . (x0 - (r / 2)) by A7, A11, A19, A36, RFUNCT_2:21; then 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:50; then 0 < min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by A37, XXREAL_0:15; then reconsider N1 = ].(r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))),(r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))).[ as Neighbourhood of r1 by RCOMP_1:def_6; take N1 = N1; ::_thesis: N1 c= rng (f | (left_open_halfline p)) f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by A17, A21, A19, A36, RFUNCT_2:21; then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29; then A38: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ; thus N1 c= rng (f | (left_open_halfline p)) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng (f | (left_open_halfline p)) ) A39: ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25; assume x in N1 ; ::_thesis: x in rng (f | (left_open_halfline p)) then consider r2 being Real such that A40: r2 = x and A41: (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) < r2 and A42: r2 < (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by A6; min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . (x0 - (r / 2))) - (f . x0) by XXREAL_0:17; then (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by XREAL_1:7; then A43: r2 < f . (x0 - (r / 2)) by A42, XXREAL_0:2; min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . x0) - (f . (x0 + (r / 2))) by XXREAL_0:17; then (f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by XREAL_1:13; then f . (x0 + (r / 2)) < r2 by A41, XXREAL_0:2; then r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A43; then consider s being Real 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) /\ (left_open_halfline p) by A8, A14, XBOOLE_0:def_4; then A46: s in dom (f | (left_open_halfline p)) by RELAT_1:61; then x = (f | (left_open_halfline p)) . s by A45, FUNCT_1:47; hence x in rng (f | (left_open_halfline p)) by A46, FUNCT_1:def_3; ::_thesis: verum end; end; end; end; hence ex N being Neighbourhood of r1 st N c= rng (f | (left_open_halfline p)) ; ::_thesis: verum end; hence rng (f | (left_open_halfline p)) is open by RCOMP_1:20; ::_thesis: verum end; theorem :: FCONT_3:25 for p being Real for f being PartFunc of REAL,REAL st 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 ) holds rng (f | (right_open_halfline p)) is open proof let p be Real; ::_thesis: for f being PartFunc of REAL,REAL st 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 ) holds rng (f | (right_open_halfline p)) is open let f be PartFunc of REAL,REAL; ::_thesis: ( 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 ) set L = right_open_halfline p; assume that A1: right_open_halfline p c= dom f and A2: f | (right_open_halfline p) is continuous and A3: ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) ; ::_thesis: rng (f | (right_open_halfline p)) is open now__::_thesis:_for_r1_being_real_number_st_r1_in_rng_(f_|_(right_open_halfline_p))_holds_ ex_N_being_Neighbourhood_of_r1_st_N_c=_rng_(f_|_(right_open_halfline_p)) let r1 be real number ; ::_thesis: ( r1 in rng (f | (right_open_halfline p)) implies ex N being Neighbourhood of r1 st N c= rng (f | (right_open_halfline p)) ) set f1 = f | (right_open_halfline p); assume r1 in rng (f | (right_open_halfline p)) ; ::_thesis: ex N being Neighbourhood of r1 st N c= rng (f | (right_open_halfline p)) then consider x0 being Real such that A4: x0 in dom (f | (right_open_halfline p)) and A5: (f | (right_open_halfline p)) . x0 = r1 by PARTFUN1:3; A6: r1 = f . x0 by A4, A5, FUNCT_1:47; A7: x0 in (dom f) /\ (right_open_halfline p) by A4, RELAT_1:61; then x0 in right_open_halfline p by XBOOLE_0:def_4; then consider N being Neighbourhood of x0 such that A8: N c= right_open_halfline p by RCOMP_1:18; consider r being real number such that A9: 0 < r and A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6; reconsider r = r as 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, XBOOLE_1:1; 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 (right_open_halfline p) /\ (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 (right_open_halfline p) /\ (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= right_open_halfline p by A8, A10, A18, A20, XXREAL_2:def_12; now__::_thesis:_ex_N1_being_Neighbourhood_of_r1_st_N1_c=_rng_(f_|_(right_open_halfline_p)) percases ( f | (right_open_halfline p) is increasing or f | (right_open_halfline p) is decreasing ) by A3; supposeA25: f | (right_open_halfline p) is increasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | (right_open_halfline p)) set R = min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))); f . x0 < f . (x0 + (r / 2)) by A7, A16, A21, A25, RFUNCT_2:20; then A26: 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:50; f . (x0 - (r / 2)) < f . x0 by A7, A11, A19, A25, RFUNCT_2:20; then 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:50; then 0 < min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by A26, XXREAL_0:15; then reconsider N1 = ].(r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))),(r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))).[ as Neighbourhood of r1 by RCOMP_1:def_6; take N1 = N1; ::_thesis: N1 c= rng (f | (right_open_halfline p)) f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by A17, A21, A19, A25, RFUNCT_2:20; then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29; then A27: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ; thus N1 c= rng (f | (right_open_halfline p)) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng (f | (right_open_halfline p)) ) A28: ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] by XXREAL_1:25; assume x in N1 ; ::_thesis: x in rng (f | (right_open_halfline p)) then consider r2 being Real such that A29: r2 = x and A30: (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) < r2 and A31: r2 < (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by A6; min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . (x0 + (r / 2))) - (f . x0) by XXREAL_0:17; then (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by XREAL_1:7; then A32: r2 < f . (x0 + (r / 2)) by A31, XXREAL_0:2; min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) - (f . (x0 - (r / 2))) by XXREAL_0:17; then (f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) <= (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by XREAL_1:13; then f . (x0 - (r / 2)) < r2 by A30, XXREAL_0:2; then r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A32; then consider s being Real 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) /\ (right_open_halfline p) by A8, A14, XBOOLE_0:def_4; then A35: s in dom (f | (right_open_halfline p)) by RELAT_1:61; then x = (f | (right_open_halfline p)) . s by A34, FUNCT_1:47; hence x in rng (f | (right_open_halfline p)) by A35, FUNCT_1:def_3; ::_thesis: verum end; end; supposeA36: f | (right_open_halfline p) is decreasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | (right_open_halfline p)) set R = min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))); f . (x0 + (r / 2)) < f . x0 by A7, A16, A21, A36, RFUNCT_2:21; then A37: 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:50; f . x0 < f . (x0 - (r / 2)) by A7, A11, A19, A36, RFUNCT_2:21; then 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:50; then 0 < min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by A37, XXREAL_0:15; then reconsider N1 = ].(r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))),(r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))).[ as Neighbourhood of r1 by RCOMP_1:def_6; take N1 = N1; ::_thesis: N1 c= rng (f | (right_open_halfline p)) f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by A17, A21, A19, A36, RFUNCT_2:21; then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29; then A38: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ; thus N1 c= rng (f | (right_open_halfline p)) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng (f | (right_open_halfline p)) ) A39: ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25; assume x in N1 ; ::_thesis: x in rng (f | (right_open_halfline p)) then consider r2 being Real such that A40: r2 = x and A41: (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) < r2 and A42: r2 < (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by A6; min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . (x0 - (r / 2))) - (f . x0) by XXREAL_0:17; then (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by XREAL_1:7; then A43: r2 < f . (x0 - (r / 2)) by A42, XXREAL_0:2; min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . x0) - (f . (x0 + (r / 2))) by XXREAL_0:17; then (f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by XREAL_1:13; then f . (x0 + (r / 2)) < r2 by A41, XXREAL_0:2; then r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A43; then consider s being Real 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) /\ (right_open_halfline p) by A8, A14, XBOOLE_0:def_4; then A46: s in dom (f | (right_open_halfline p)) by RELAT_1:61; then x = (f | (right_open_halfline p)) . s by A45, FUNCT_1:47; hence x in rng (f | (right_open_halfline p)) by A46, FUNCT_1:def_3; ::_thesis: verum end; end; end; end; hence ex N being Neighbourhood of r1 st N c= rng (f | (right_open_halfline p)) ; ::_thesis: verum end; hence rng (f | (right_open_halfline p)) is open by RCOMP_1:20; ::_thesis: verum end; theorem :: FCONT_3:26 for f being PartFunc of REAL,REAL st [#] REAL c= dom f & f | ([#] REAL) is continuous & ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) holds rng f is open proof let f be PartFunc of REAL,REAL; ::_thesis: ( [#] REAL c= dom f & f | ([#] REAL) is continuous & ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) implies rng f is open ) set L = [#] REAL; assume that A1: [#] REAL c= dom f and A2: f | ([#] REAL) is continuous and A3: ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) ; ::_thesis: rng f is open now__::_thesis:_for_r1_being_real_number_st_r1_in_rng_f_holds_ ex_N_being_Neighbourhood_of_r1_st_N_c=_rng_f let r1 be real number ; ::_thesis: ( r1 in rng f implies ex N being Neighbourhood of r1 st N c= rng f ) assume r1 in rng f ; ::_thesis: ex N being Neighbourhood of r1 st N c= rng f then consider x0 being Real such that A4: x0 in dom f and A5: f . x0 = r1 by PARTFUN1:3; A6: x0 in ([#] REAL) /\ (dom f) by A4, XBOOLE_0:def_4; set N = the Neighbourhood of x0; consider r being real number such that A7: 0 < r and A8: the Neighbourhood of x0 = ].(x0 - r),(x0 + r).[ by RCOMP_1:def_6; reconsider r = r as 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: the Neighbourhood of x0 c= dom f by A1, XBOOLE_1:1; 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 ([#] REAL) /\ (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 ([#] REAL) /\ (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__::_thesis:_ex_N1_being_Neighbourhood_of_r1_st_N1_c=_rng_f percases ( f | ([#] REAL) is increasing or f | ([#] REAL) is decreasing ) by A3; supposeA22: f | ([#] REAL) is increasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng f set R = min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))); f . x0 < f . (x0 + (r / 2)) by A15, A18, A6, A22, RFUNCT_2:20; then A23: 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:50; f . (x0 - (r / 2)) < f . x0 by A9, A20, A6, A22, RFUNCT_2:20; then 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:50; then 0 < min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by A23, XXREAL_0:15; then reconsider N1 = ].(r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))),(r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))).[ as Neighbourhood of r1 by RCOMP_1:def_6; take N1 = N1; ::_thesis: N1 c= rng f f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by A16, A18, A20, A22, RFUNCT_2:20; then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29; then A24: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ; thus N1 c= rng f ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng f ) A25: ( [.(x0 - (r / 2)),(x0 + (r / 2)).] c= dom f & ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ) by A1, XBOOLE_1:1, XXREAL_1:25; assume x in N1 ; ::_thesis: x in rng f then consider r2 being Real such that A26: r2 = x and A27: (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) < r2 and A28: r2 < (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by A5; min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . (x0 + (r / 2))) - (f . x0) by XXREAL_0:17; then (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by XREAL_1:7; then A29: r2 < f . (x0 + (r / 2)) by A28, XXREAL_0:2; min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) - (f . (x0 - (r / 2))) by XXREAL_0:17; then (f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) <= (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by XREAL_1:13; then f . (x0 - (r / 2)) < r2 by A27, XXREAL_0:2; then r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A29; then consider s being Real 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 the Neighbourhood of x0 by A8, A21, A30; hence x in rng f by A13, A31, FUNCT_1:def_3; ::_thesis: verum end; end; supposeA32: f | ([#] REAL) is decreasing ; ::_thesis: ex N1 being Neighbourhood of r1 st N1 c= rng f set R = min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))); f . (x0 + (r / 2)) < f . x0 by A15, A18, A6, A32, RFUNCT_2:21; then A33: 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:50; f . x0 < f . (x0 - (r / 2)) by A9, A20, A6, A32, RFUNCT_2:21; then 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:50; then 0 < min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by A33, XXREAL_0:15; then reconsider N1 = ].(r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))),(r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))).[ as Neighbourhood of r1 by RCOMP_1:def_6; take N1 = N1; ::_thesis: N1 c= rng f f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by A16, A18, A20, A32, RFUNCT_2:21; then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29; then A34: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ; thus N1 c= rng f ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N1 or x in rng f ) A35: ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25; assume x in N1 ; ::_thesis: x in rng f then consider r2 being Real such that A36: r2 = x and A37: (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) < r2 and A38: r2 < (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by A5; min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . (x0 - (r / 2))) - (f . x0) by XXREAL_0:17; then (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by XREAL_1:7; then A39: r2 < f . (x0 - (r / 2)) by A38, XXREAL_0:2; min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . x0) - (f . (x0 + (r / 2))) by XXREAL_0:17; then (f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by XREAL_1:13; then f . (x0 + (r / 2)) < r2 by A37, XXREAL_0:2; then r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A39; then consider s being Real 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 the Neighbourhood of x0 by A8, A21, A40; hence x in rng f by A13, A41, FUNCT_1:def_3; ::_thesis: verum end; end; end; end; hence ex N being Neighbourhood of r1 st N c= rng f ; ::_thesis: verum end; hence rng f is open by RCOMP_1:20; ::_thesis: verum end;