:: FCONT_2 semantic presentation begin definition let f be PartFunc of REAL,REAL; attrf is uniformly_continuous means :Def1: :: FCONT_2:def 1 for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom f & x2 in dom f & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ); end; :: deftheorem Def1 defines uniformly_continuous FCONT_2:def_1_:_ for f being PartFunc of REAL,REAL holds ( f is uniformly_continuous iff for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom f & x2 in dom f & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) ); theorem Th1: :: FCONT_2:1 for X being set for f being PartFunc of REAL,REAL holds ( f | X is uniformly_continuous iff for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) ) proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL holds ( f | X is uniformly_continuous iff for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is uniformly_continuous iff for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) ) thus ( f | X is uniformly_continuous implies for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) ) ::_thesis: ( ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) ) implies f | X is uniformly_continuous ) proof assume A1: f | X is uniformly_continuous ; ::_thesis: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) then consider s being Real such that A2: 0 < s and A3: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs (((f | X) . x1) - ((f | X) . x2)) < r by A1, Def1; take s ; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) thus 0 < s by A2; ::_thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r let x1, x2 be Real; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s implies abs ((f . x1) - (f . x2)) < r ) assume that A4: x1 in dom (f | X) and A5: x2 in dom (f | X) ; ::_thesis: ( not abs (x1 - x2) < s or abs ((f . x1) - (f . x2)) < r ) A6: (f | X) . x2 = f . x2 by A5, FUNCT_1:47; (f | X) . x1 = f . x1 by A4, FUNCT_1:47; hence ( not abs (x1 - x2) < s or abs ((f . x1) - (f . x2)) < r ) by A3, A4, A5, A6; ::_thesis: verum end; assume A7: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) ; ::_thesis: f | X is uniformly_continuous let r be Real; :: according to FCONT_2:def_1 ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs (((f | X) . x1) - ((f | X) . x2)) < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs (((f | X) . x1) - ((f | X) . x2)) < r ) ) then consider s being Real such that A8: 0 < s and A9: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r by A7; take s ; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs (((f | X) . x1) - ((f | X) . x2)) < r ) ) thus 0 < s by A8; ::_thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs (((f | X) . x1) - ((f | X) . x2)) < r let x1, x2 be Real; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s implies abs (((f | X) . x1) - ((f | X) . x2)) < r ) assume that A10: x1 in dom (f | X) and A11: x2 in dom (f | X) ; ::_thesis: ( not abs (x1 - x2) < s or abs (((f | X) . x1) - ((f | X) . x2)) < r ) A12: (f | X) . x2 = f . x2 by A11, FUNCT_1:47; (f | X) . x1 = f . x1 by A10, FUNCT_1:47; hence ( not abs (x1 - x2) < s or abs (((f | X) . x1) - ((f | X) . x2)) < r ) by A9, A10, A11, A12; ::_thesis: verum end; theorem Th2: :: FCONT_2:2 for X, X1 being set for f being PartFunc of REAL,REAL st f | X is uniformly_continuous & X1 c= X holds f | X1 is uniformly_continuous proof let X, X1 be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is uniformly_continuous & X1 c= X holds f | X1 is uniformly_continuous let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is uniformly_continuous & X1 c= X implies f | X1 is uniformly_continuous ) assume that A1: f | X is uniformly_continuous and A2: X1 c= X ; ::_thesis: f | X1 is uniformly_continuous now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_s_being_Real_st_ (_0_<_s_&_(_for_x1,_x2_being_Real_st_x1_in_dom_(f_|_X1)_&_x2_in_dom_(f_|_X1)_&_abs_(x1_-_x2)_<_s_holds_ abs_((f_._x1)_-_(f_._x2))_<_r_)_) let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X1) & x2 in dom (f | X1) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X1) & x2 in dom (f | X1) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) then consider s being Real such that A3: 0 < s and A4: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r by A1, Th1; take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X1) & x2 in dom (f | X1) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r ) ) thus 0 < s by A3; ::_thesis: for x1, x2 being Real st x1 in dom (f | X1) & x2 in dom (f | X1) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r let x1, x2 be Real; ::_thesis: ( x1 in dom (f | X1) & x2 in dom (f | X1) & abs (x1 - x2) < s implies abs ((f . x1) - (f . x2)) < r ) assume that A5: x1 in dom (f | X1) and A6: x2 in dom (f | X1) and A7: abs (x1 - x2) < s ; ::_thesis: abs ((f . x1) - (f . x2)) < r f | X1 c= f | X by A2, RELAT_1:75; then dom (f | X1) c= dom (f | X) by RELAT_1:11; hence abs ((f . x1) - (f . x2)) < r by A4, A5, A6, A7; ::_thesis: verum end; hence f | X1 is uniformly_continuous by Th1; ::_thesis: verum end; theorem :: FCONT_2:3 for X, X1 being set for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous holds (f1 + f2) | (X /\ X1) is uniformly_continuous proof let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous holds (f1 + f2) | (X /\ X1) is uniformly_continuous let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous implies (f1 + f2) | (X /\ X1) is uniformly_continuous ) assume that A1: X c= dom f1 and A2: X1 c= dom f2 ; ::_thesis: ( not f1 | X is uniformly_continuous or not f2 | X1 is uniformly_continuous or (f1 + f2) | (X /\ X1) is uniformly_continuous ) A3: X /\ X1 c= dom f2 by A2, XBOOLE_1:108; X /\ X1 c= dom f1 by A1, XBOOLE_1:108; then X /\ X1 c= (dom f1) /\ (dom f2) by A3, XBOOLE_1:19; then A4: X /\ X1 c= dom (f1 + f2) by VALUED_1:def_1; assume that A5: f1 | X is uniformly_continuous and A6: f2 | X1 is uniformly_continuous ; ::_thesis: (f1 + f2) | (X /\ X1) is uniformly_continuous A7: f2 | (X /\ X1) is uniformly_continuous by A6, Th2, XBOOLE_1:17; A8: f1 | (X /\ X1) is uniformly_continuous by A5, Th2, XBOOLE_1:17; now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_p_being_Element_of_REAL_st_ (_0_<_p_&_(_for_x1,_x2_being_Real_st_x1_in_dom_((f1_+_f2)_|_(X_/\_X1))_&_x2_in_dom_((f1_+_f2)_|_(X_/\_X1))_&_abs_(x1_-_x2)_<_p_holds_ abs_(((f1_+_f2)_._x1)_-_((f1_+_f2)_._x2))_<_r_)_) let r be Real; ::_thesis: ( 0 < r implies ex p being Element of REAL st ( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p holds abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r ) ) ) A9: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1; assume 0 < r ; ::_thesis: ex p being Element of REAL st ( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p holds abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r ) ) then A10: 0 < r / 2 by XREAL_1:215; then consider s being Real such that A11: 0 < s and A12: for x1, x2 being Real st x1 in dom (f1 | (X /\ X1)) & x2 in dom (f1 | (X /\ X1)) & abs (x1 - x2) < s holds abs ((f1 . x1) - (f1 . x2)) < r / 2 by A8, Th1; consider g being Real such that A13: 0 < g and A14: for x1, x2 being Real st x1 in dom (f2 | (X /\ X1)) & x2 in dom (f2 | (X /\ X1)) & abs (x1 - x2) < g holds abs ((f2 . x1) - (f2 . x2)) < r / 2 by A7, A10, Th1; take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p holds abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r ) ) thus 0 < p by A11, A13, XXREAL_0:15; ::_thesis: for x1, x2 being Real st x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p holds abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r let x1, x2 be Real; ::_thesis: ( x1 in dom ((f1 + f2) | (X /\ X1)) & x2 in dom ((f1 + f2) | (X /\ X1)) & abs (x1 - x2) < p implies abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r ) assume that A15: x1 in dom ((f1 + f2) | (X /\ X1)) and A16: x2 in dom ((f1 + f2) | (X /\ X1)) and A17: abs (x1 - x2) < p ; ::_thesis: abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r A18: x2 in X /\ X1 by A16, RELAT_1:57; A19: x2 in dom (f1 + f2) by A16, RELAT_1:57; then x2 in dom f2 by A9, XBOOLE_0:def_4; then A20: x2 in dom (f2 | (X /\ X1)) by A18, RELAT_1:57; p <= g by XXREAL_0:17; then A21: abs (x1 - x2) < g by A17, XXREAL_0:2; A22: x1 in X /\ X1 by A15, RELAT_1:57; x2 in dom f1 by A9, A19, XBOOLE_0:def_4; then A23: x2 in dom (f1 | (X /\ X1)) by A18, RELAT_1:57; p <= s by XXREAL_0:17; then A24: abs (x1 - x2) < s by A17, XXREAL_0:2; A25: x1 in dom (f1 + f2) by A15, RELAT_1:57; then x1 in dom f2 by A9, XBOOLE_0:def_4; then x1 in dom (f2 | (X /\ X1)) by A22, RELAT_1:57; then A26: abs ((f2 . x1) - (f2 . x2)) < r / 2 by A14, A21, A20; x1 in dom f1 by A9, A25, XBOOLE_0:def_4; then x1 in dom (f1 | (X /\ X1)) by A22, RELAT_1:57; then abs ((f1 . x1) - (f1 . x2)) < r / 2 by A12, A24, A23; then A27: (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) < (r / 2) + (r / 2) by A26, XREAL_1:8; A28: abs (((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))) <= (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) by COMPLEX1:56; abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) = abs (((f1 . x1) + (f2 . x1)) - ((f1 + f2) . x2)) by A4, A22, VALUED_1:def_1 .= abs (((f1 . x1) + (f2 . x1)) - ((f1 . x2) + (f2 . x2))) by A4, A18, VALUED_1:def_1 .= abs (((f1 . x1) - (f1 . x2)) + ((f2 . x1) - (f2 . x2))) ; hence abs (((f1 + f2) . x1) - ((f1 + f2) . x2)) < r by A27, A28, XXREAL_0:2; ::_thesis: verum end; hence (f1 + f2) | (X /\ X1) is uniformly_continuous by Th1; ::_thesis: verum end; theorem :: FCONT_2:4 for X, X1 being set for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous holds (f1 - f2) | (X /\ X1) is uniformly_continuous proof let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous holds (f1 - f2) | (X /\ X1) is uniformly_continuous let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous implies (f1 - f2) | (X /\ X1) is uniformly_continuous ) assume that A1: X c= dom f1 and A2: X1 c= dom f2 ; ::_thesis: ( not f1 | X is uniformly_continuous or not f2 | X1 is uniformly_continuous or (f1 - f2) | (X /\ X1) is uniformly_continuous ) A3: X /\ X1 c= dom f2 by A2, XBOOLE_1:108; X /\ X1 c= dom f1 by A1, XBOOLE_1:108; then X /\ X1 c= (dom f1) /\ (dom f2) by A3, XBOOLE_1:19; then A4: X /\ X1 c= dom (f1 - f2) by VALUED_1:12; assume that A5: f1 | X is uniformly_continuous and A6: f2 | X1 is uniformly_continuous ; ::_thesis: (f1 - f2) | (X /\ X1) is uniformly_continuous A7: f2 | (X /\ X1) is uniformly_continuous by A6, Th2, XBOOLE_1:17; A8: f1 | (X /\ X1) is uniformly_continuous by A5, Th2, XBOOLE_1:17; now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_p_being_Element_of_REAL_st_ (_0_<_p_&_(_for_x1,_x2_being_Real_st_x1_in_dom_((f1_-_f2)_|_(X_/\_X1))_&_x2_in_dom_((f1_-_f2)_|_(X_/\_X1))_&_abs_(x1_-_x2)_<_p_holds_ abs_(((f1_-_f2)_._x1)_-_((f1_-_f2)_._x2))_<_r_)_) let r be Real; ::_thesis: ( 0 < r implies ex p being Element of REAL st ( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 - f2) | (X /\ X1)) & x2 in dom ((f1 - f2) | (X /\ X1)) & abs (x1 - x2) < p holds abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r ) ) ) A9: dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_1:12; assume 0 < r ; ::_thesis: ex p being Element of REAL st ( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 - f2) | (X /\ X1)) & x2 in dom ((f1 - f2) | (X /\ X1)) & abs (x1 - x2) < p holds abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r ) ) then A10: 0 < r / 2 by XREAL_1:215; then consider s being Real such that A11: 0 < s and A12: for x1, x2 being Real st x1 in dom (f1 | (X /\ X1)) & x2 in dom (f1 | (X /\ X1)) & abs (x1 - x2) < s holds abs ((f1 . x1) - (f1 . x2)) < r / 2 by A8, Th1; consider g being Real such that A13: 0 < g and A14: for x1, x2 being Real st x1 in dom (f2 | (X /\ X1)) & x2 in dom (f2 | (X /\ X1)) & abs (x1 - x2) < g holds abs ((f2 . x1) - (f2 . x2)) < r / 2 by A7, A10, Th1; take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 - f2) | (X /\ X1)) & x2 in dom ((f1 - f2) | (X /\ X1)) & abs (x1 - x2) < p holds abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r ) ) thus 0 < p by A11, A13, XXREAL_0:15; ::_thesis: for x1, x2 being Real st x1 in dom ((f1 - f2) | (X /\ X1)) & x2 in dom ((f1 - f2) | (X /\ X1)) & abs (x1 - x2) < p holds abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r let x1, x2 be Real; ::_thesis: ( x1 in dom ((f1 - f2) | (X /\ X1)) & x2 in dom ((f1 - f2) | (X /\ X1)) & abs (x1 - x2) < p implies abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r ) assume that A15: x1 in dom ((f1 - f2) | (X /\ X1)) and A16: x2 in dom ((f1 - f2) | (X /\ X1)) and A17: abs (x1 - x2) < p ; ::_thesis: abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r A18: x2 in X /\ X1 by A16, RELAT_1:57; A19: x2 in dom (f1 - f2) by A16, RELAT_1:57; then x2 in dom f2 by A9, XBOOLE_0:def_4; then A20: x2 in dom (f2 | (X /\ X1)) by A18, RELAT_1:57; p <= g by XXREAL_0:17; then A21: abs (x1 - x2) < g by A17, XXREAL_0:2; A22: x1 in X /\ X1 by A15, RELAT_1:57; x2 in dom f1 by A9, A19, XBOOLE_0:def_4; then A23: x2 in dom (f1 | (X /\ X1)) by A18, RELAT_1:57; p <= s by XXREAL_0:17; then A24: abs (x1 - x2) < s by A17, XXREAL_0:2; A25: x1 in dom (f1 - f2) by A15, RELAT_1:57; then x1 in dom f2 by A9, XBOOLE_0:def_4; then x1 in dom (f2 | (X /\ X1)) by A22, RELAT_1:57; then A26: abs ((f2 . x1) - (f2 . x2)) < r / 2 by A14, A21, A20; x1 in dom f1 by A9, A25, XBOOLE_0:def_4; then x1 in dom (f1 | (X /\ X1)) by A22, RELAT_1:57; then abs ((f1 . x1) - (f1 . x2)) < r / 2 by A12, A24, A23; then A27: (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) < (r / 2) + (r / 2) by A26, XREAL_1:8; A28: abs (((f1 . x1) - (f1 . x2)) - ((f2 . x1) - (f2 . x2))) <= (abs ((f1 . x1) - (f1 . x2))) + (abs ((f2 . x1) - (f2 . x2))) by COMPLEX1:57; abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) = abs (((f1 . x1) - (f2 . x1)) - ((f1 - f2) . x2)) by A4, A22, VALUED_1:13 .= abs (((f1 . x1) - (f2 . x1)) - ((f1 . x2) - (f2 . x2))) by A4, A18, VALUED_1:13 .= abs (((f1 . x1) - (f1 . x2)) - ((f2 . x1) - (f2 . x2))) ; hence abs (((f1 - f2) . x1) - ((f1 - f2) . x2)) < r by A27, A28, XXREAL_0:2; ::_thesis: verum end; hence (f1 - f2) | (X /\ X1) is uniformly_continuous by Th1; ::_thesis: verum end; theorem Th5: :: FCONT_2:5 for X being set for p being Real for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds (p (#) f) | X is uniformly_continuous proof let X be set ; ::_thesis: for p being Real for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds (p (#) f) | X is uniformly_continuous let p be Real; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds (p (#) f) | X is uniformly_continuous let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is uniformly_continuous implies (p (#) f) | X is uniformly_continuous ) assume X c= dom f ; ::_thesis: ( not f | X is uniformly_continuous or (p (#) f) | X is uniformly_continuous ) then A1: X c= dom (p (#) f) by VALUED_1:def_5; assume A2: f | X is uniformly_continuous ; ::_thesis: (p (#) f) | X is uniformly_continuous percases ( p = 0 or p <> 0 ) ; supposeA3: p = 0 ; ::_thesis: (p (#) f) | X is uniformly_continuous now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_s_being_Real_st_ (_0_<_s_&_(_for_x1,_x2_being_Real_st_x1_in_dom_((p_(#)_f)_|_X)_&_x2_in_dom_((p_(#)_f)_|_X)_&_abs_(x1_-_x2)_<_s_holds_ abs_(((p_(#)_f)_._x1)_-_((p_(#)_f)_._x2))_<_r_)_) let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) ) ) assume A4: 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) ) then consider s being Real such that A5: 0 < s and for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r by A2, Th1; take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) ) thus 0 < s by A5; ::_thesis: for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r let x1, x2 be Real; ::_thesis: ( x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s implies abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) assume that A6: x1 in dom ((p (#) f) | X) and A7: x2 in dom ((p (#) f) | X) and abs (x1 - x2) < s ; ::_thesis: abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r A8: x2 in X by A7, RELAT_1:57; x1 in X by A6, RELAT_1:57; then abs (((p (#) f) . x1) - ((p (#) f) . x2)) = abs ((p * (f . x1)) - ((p (#) f) . x2)) by A1, VALUED_1:def_5 .= abs (0 - (p * (f . x2))) by A1, A3, A8, VALUED_1:def_5 .= 0 by A3, ABSVALUE:2 ; hence abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r by A4; ::_thesis: verum end; hence (p (#) f) | X is uniformly_continuous by Th1; ::_thesis: verum end; supposeA9: p <> 0 ; ::_thesis: (p (#) f) | X is uniformly_continuous then A10: 0 < abs p by COMPLEX1:47; A11: 0 <> abs p by A9, COMPLEX1:47; now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_s_being_Real_st_ (_0_<_s_&_(_for_x1,_x2_being_Real_st_x1_in_dom_((p_(#)_f)_|_X)_&_x2_in_dom_((p_(#)_f)_|_X)_&_abs_(x1_-_x2)_<_s_holds_ abs_(((p_(#)_f)_._x1)_-_((p_(#)_f)_._x2))_<_r_)_) let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) ) then 0 < r / (abs p) by A10, XREAL_1:139; then consider s being Real such that A12: 0 < s and A13: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r / (abs p) by A2, Th1; take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) ) thus 0 < s by A12; ::_thesis: for x1, x2 being Real st x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s holds abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r let x1, x2 be Real; ::_thesis: ( x1 in dom ((p (#) f) | X) & x2 in dom ((p (#) f) | X) & abs (x1 - x2) < s implies abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r ) assume that A14: x1 in dom ((p (#) f) | X) and A15: x2 in dom ((p (#) f) | X) and A16: abs (x1 - x2) < s ; ::_thesis: abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r A17: x2 in X by A15, RELAT_1:57; A18: x1 in X by A14, RELAT_1:57; then A19: abs (((p (#) f) . x1) - ((p (#) f) . x2)) = abs ((p * (f . x1)) - ((p (#) f) . x2)) by A1, VALUED_1:def_5 .= abs ((p * (f . x1)) - (p * (f . x2))) by A1, A17, VALUED_1:def_5 .= abs (p * ((f . x1) - (f . x2))) .= (abs p) * (abs ((f . x1) - (f . x2))) by COMPLEX1:65 ; x2 in dom (p (#) f) by A15, RELAT_1:57; then x2 in dom f by VALUED_1:def_5; then A20: x2 in dom (f | X) by A17, RELAT_1:57; x1 in dom (p (#) f) by A14, RELAT_1:57; then x1 in dom f by VALUED_1:def_5; then x1 in dom (f | X) by A18, RELAT_1:57; then (abs p) * (abs ((f . x1) - (f . x2))) < (r / (abs p)) * (abs p) by A10, A13, A16, A20, XREAL_1:68; hence abs (((p (#) f) . x1) - ((p (#) f) . x2)) < r by A11, A19, XCMPLX_1:87; ::_thesis: verum end; hence (p (#) f) | X is uniformly_continuous by Th1; ::_thesis: verum end; end; end; theorem :: FCONT_2:6 for X being set for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds (- f) | X is uniformly_continuous proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous holds (- f) | X is uniformly_continuous let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is uniformly_continuous implies (- f) | X is uniformly_continuous ) assume A1: X c= dom f ; ::_thesis: ( not f | X is uniformly_continuous or (- f) | X is uniformly_continuous ) A2: - f = (- 1) (#) f ; assume f | X is uniformly_continuous ; ::_thesis: (- f) | X is uniformly_continuous hence (- f) | X is uniformly_continuous by A1, A2, Th5; ::_thesis: verum end; theorem :: FCONT_2:7 for X being set for f being PartFunc of REAL,REAL st f | X is uniformly_continuous holds (abs f) | X is uniformly_continuous proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is uniformly_continuous holds (abs f) | X is uniformly_continuous let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is uniformly_continuous implies (abs f) | X is uniformly_continuous ) assume A1: f | X is uniformly_continuous ; ::_thesis: (abs f) | X is uniformly_continuous now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_s_being_Real_st_ (_0_<_s_&_(_for_x1,_x2_being_Real_st_x1_in_dom_((abs_f)_|_X)_&_x2_in_dom_((abs_f)_|_X)_&_abs_(x1_-_x2)_<_s_holds_ abs_(((abs_f)_._x1)_-_((abs_f)_._x2))_<_r_)_) let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom ((abs f) | X) & x2 in dom ((abs f) | X) & abs (x1 - x2) < s holds abs (((abs f) . x1) - ((abs f) . x2)) < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom ((abs f) | X) & x2 in dom ((abs f) | X) & abs (x1 - x2) < s holds abs (((abs f) . x1) - ((abs f) . x2)) < r ) ) then consider s being Real such that A2: 0 < s and A3: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r by A1, Th1; take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom ((abs f) | X) & x2 in dom ((abs f) | X) & abs (x1 - x2) < s holds abs (((abs f) . x1) - ((abs f) . x2)) < r ) ) thus 0 < s by A2; ::_thesis: for x1, x2 being Real st x1 in dom ((abs f) | X) & x2 in dom ((abs f) | X) & abs (x1 - x2) < s holds abs (((abs f) . x1) - ((abs f) . x2)) < r let x1, x2 be Real; ::_thesis: ( x1 in dom ((abs f) | X) & x2 in dom ((abs f) | X) & abs (x1 - x2) < s implies abs (((abs f) . x1) - ((abs f) . x2)) < r ) assume that A4: x1 in dom ((abs f) | X) and A5: x2 in dom ((abs f) | X) and A6: abs (x1 - x2) < s ; ::_thesis: abs (((abs f) . x1) - ((abs f) . x2)) < r x2 in dom (abs f) by A5, RELAT_1:57; then A7: x2 in dom f by VALUED_1:def_11; x2 in X by A5, RELAT_1:57; then A8: x2 in dom (f | X) by A7, RELAT_1:57; abs (((abs f) . x1) - ((abs f) . x2)) = abs ((abs (f . x1)) - ((abs f) . x2)) by VALUED_1:18 .= abs ((abs (f . x1)) - (abs (f . x2))) by VALUED_1:18 ; then A9: abs (((abs f) . x1) - ((abs f) . x2)) <= abs ((f . x1) - (f . x2)) by COMPLEX1:64; x1 in dom (abs f) by A4, RELAT_1:57; then A10: x1 in dom f by VALUED_1:def_11; x1 in X by A4, RELAT_1:57; then x1 in dom (f | X) by A10, RELAT_1:57; then abs ((f . x1) - (f . x2)) < r by A3, A6, A8; hence abs (((abs f) . x1) - ((abs f) . x2)) < r by A9, XXREAL_0:2; ::_thesis: verum end; hence (abs f) | X is uniformly_continuous by Th1; ::_thesis: verum end; theorem :: FCONT_2:8 for X, X1, Z, Z1 being set for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous & f1 | Z is bounded & f2 | Z1 is bounded holds (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous proof let X, X1, Z, Z1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous & f1 | Z is bounded & f2 | Z1 is bounded holds (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f1 & X1 c= dom f2 & f1 | X is uniformly_continuous & f2 | X1 is uniformly_continuous & f1 | Z is bounded & f2 | Z1 is bounded implies (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous ) assume that A1: X c= dom f1 and A2: X1 c= dom f2 ; ::_thesis: ( not f1 | X is uniformly_continuous or not f2 | X1 is uniformly_continuous or not f1 | Z is bounded or not f2 | Z1 is bounded or (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous ) assume that A3: f1 | X is uniformly_continuous and A4: f2 | X1 is uniformly_continuous and A5: f1 | Z is bounded and A6: f2 | Z1 is bounded ; ::_thesis: (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous consider x1 being real number such that A7: for r being set st r in Z /\ (dom f1) holds abs (f1 . r) <= x1 by A5, RFUNCT_1:73; consider x2 being real number such that A8: for r being set st r in Z1 /\ (dom f2) holds abs (f2 . r) <= x2 by A6, RFUNCT_1:73; reconsider x1 = x1, x2 = x2 as Real by XREAL_0:def_1; set M1 = (abs x1) + 1; set M2 = (abs x2) + 1; set M = max (((abs x1) + 1),((abs x2) + 1)); A9: now__::_thesis:_for_r_being_Real_st_r_in_((X_/\_Z)_/\_X1)_/\_Z1_holds_ (_abs_(f1_._r)_<_max_(((abs_x1)_+_1),((abs_x2)_+_1))_&_abs_(f2_._r)_<_max_(((abs_x1)_+_1),((abs_x2)_+_1))_) let r be Real; ::_thesis: ( r in ((X /\ Z) /\ X1) /\ Z1 implies ( abs (f1 . r) < max (((abs x1) + 1),((abs x2) + 1)) & abs (f2 . r) < max (((abs x1) + 1),((abs x2) + 1)) ) ) A10: (abs x1) + 1 <= max (((abs x1) + 1),((abs x2) + 1)) by XXREAL_0:25; assume r in ((X /\ Z) /\ X1) /\ Z1 ; ::_thesis: ( abs (f1 . r) < max (((abs x1) + 1),((abs x2) + 1)) & abs (f2 . r) < max (((abs x1) + 1),((abs x2) + 1)) ) then A11: r in (X /\ Z) /\ (X1 /\ Z1) by XBOOLE_1:16; then A12: r in X /\ Z by XBOOLE_0:def_4; then A13: r in Z by XBOOLE_0:def_4; r in X by A12, XBOOLE_0:def_4; then r in Z /\ (dom f1) by A1, A13, XBOOLE_0:def_4; then A14: abs (f1 . r) <= x1 by A7; x1 + 0 < (abs x1) + 1 by ABSVALUE:4, XREAL_1:8; then abs (f1 . r) < (abs x1) + 1 by A14, XXREAL_0:2; hence abs (f1 . r) < max (((abs x1) + 1),((abs x2) + 1)) by A10, XXREAL_0:2; ::_thesis: abs (f2 . r) < max (((abs x1) + 1),((abs x2) + 1)) A15: (abs x2) + 1 <= max (((abs x1) + 1),((abs x2) + 1)) by XXREAL_0:25; A16: r in X1 /\ Z1 by A11, XBOOLE_0:def_4; then A17: r in Z1 by XBOOLE_0:def_4; r in X1 by A16, XBOOLE_0:def_4; then r in Z1 /\ (dom f2) by A2, A17, XBOOLE_0:def_4; then A18: abs (f2 . r) <= x2 by A8; x2 + 0 < (abs x2) + 1 by ABSVALUE:4, XREAL_1:8; then abs (f2 . r) < (abs x2) + 1 by A18, XXREAL_0:2; hence abs (f2 . r) < max (((abs x1) + 1),((abs x2) + 1)) by A15, XXREAL_0:2; ::_thesis: verum end; A19: 0 + 0 < (abs x2) + 1 by COMPLEX1:46, XREAL_1:8; 0 + 0 < (abs x1) + 1 by COMPLEX1:46, XREAL_1:8; then A20: 0 < max (((abs x1) + 1),((abs x2) + 1)) by A19, XXREAL_0:16; then A21: 0 < 2 * (max (((abs x1) + 1),((abs x2) + 1))) by XREAL_1:129; for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < s holds abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r ) ) proof let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < s holds abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < s holds abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r ) ) then A22: 0 < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A21, XREAL_1:139; then consider s being Real such that A23: 0 < s and A24: for x1, x2 being Real st x1 in dom (f1 | X) & x2 in dom (f1 | X) & abs (x1 - x2) < s holds abs ((f1 . x1) - (f1 . x2)) < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A3, Th1; consider g being Real such that A25: 0 < g and A26: for x1, x2 being Real st x1 in dom (f2 | X1) & x2 in dom (f2 | X1) & abs (x1 - x2) < g holds abs ((f2 . x1) - (f2 . x2)) < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A4, A22, Th1; take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < p holds abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r ) ) thus 0 < p by A23, A25, XXREAL_0:15; ::_thesis: for x1, x2 being Real st x1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & x2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (x1 - x2) < p holds abs (((f1 (#) f2) . x1) - ((f1 (#) f2) . x2)) < r let y1, y2 be Real; ::_thesis: ( y1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & y2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) & abs (y1 - y2) < p implies abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r ) assume that A27: y1 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) and A28: y2 in dom ((f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1)) ; ::_thesis: ( not abs (y1 - y2) < p or abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r ) assume A29: abs (y1 - y2) < p ; ::_thesis: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r A30: y2 in ((X /\ Z) /\ X1) /\ Z1 by A28, RELAT_1:57; then A31: y2 in (X /\ Z) /\ (X1 /\ Z1) by XBOOLE_1:16; then y2 in X /\ Z by XBOOLE_0:def_4; then y2 in X by XBOOLE_0:def_4; then A32: y2 in dom (f1 | X) by A1, RELAT_1:62; A33: y1 in ((X /\ Z) /\ X1) /\ Z1 by A27, RELAT_1:57; then A34: y1 in (X /\ Z) /\ (X1 /\ Z1) by XBOOLE_1:16; then y1 in X /\ Z by XBOOLE_0:def_4; then y1 in X by XBOOLE_0:def_4; then A35: y1 in dom (f1 | X) by A1, RELAT_1:62; y2 in X1 /\ Z1 by A31, XBOOLE_0:def_4; then y2 in X1 by XBOOLE_0:def_4; then A36: y2 in dom (f2 | X1) by A2, RELAT_1:62; y1 in X1 /\ Z1 by A34, XBOOLE_0:def_4; then y1 in X1 by XBOOLE_0:def_4; then A37: y1 in dom (f2 | X1) by A2, RELAT_1:62; p <= g by XXREAL_0:17; then abs (y1 - y2) < g by A29, XXREAL_0:2; then A38: abs ((f2 . y1) - (f2 . y2)) < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A26, A37, A36; abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) = abs (((f1 . y1) * (f2 . y1)) - ((f1 (#) f2) . y2)) by VALUED_1:5 .= abs ((((f1 . y1) * (f2 . y1)) + (((f1 . y1) * (f2 . y2)) - ((f1 . y1) * (f2 . y2)))) - ((f1 . y2) * (f2 . y2))) by VALUED_1:5 .= abs (((f1 . y1) * ((f2 . y1) - (f2 . y2))) + (((f1 . y1) - (f1 . y2)) * (f2 . y2))) ; then A39: abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) <= (abs ((f1 . y1) * ((f2 . y1) - (f2 . y2)))) + (abs (((f1 . y1) - (f1 . y2)) * (f2 . y2))) by COMPLEX1:56; A40: abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) = (abs (f1 . y1)) * (abs ((f2 . y1) - (f2 . y2))) by COMPLEX1:65; A41: abs (f2 . y2) < max (((abs x1) + 1),((abs x2) + 1)) by A9, A30; A42: 0 <= abs (f2 . y2) by COMPLEX1:46; A43: 0 <= abs ((f1 . y1) - (f1 . y2)) by COMPLEX1:46; A44: abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) = (abs (f2 . y2)) * (abs ((f1 . y1) - (f1 . y2))) by COMPLEX1:65; p <= s by XXREAL_0:17; then abs (y1 - y2) < s by A29, XXREAL_0:2; then abs ((f1 . y1) - (f1 . y2)) < r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))) by A24, A35, A32; then A45: abs (((f1 . y1) - (f1 . y2)) * (f2 . y2)) < (max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1))))) by A44, A41, A43, A42, XREAL_1:96; A46: 0 <= abs (f1 . y1) by COMPLEX1:46; A47: 0 <= abs ((f2 . y1) - (f2 . y2)) by COMPLEX1:46; abs (f1 . y1) < max (((abs x1) + 1),((abs x2) + 1)) by A9, A33; then abs ((f1 . y1) * ((f2 . y1) - (f2 . y2))) < (max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1))))) by A40, A38, A47, A46, XREAL_1:96; then A48: (abs ((f1 . y1) * ((f2 . y1) - (f2 . y2)))) + (abs (((f1 . y1) - (f1 . y2)) * (f2 . y2))) < ((max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))))) + ((max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))))) by A45, XREAL_1:8; ((max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))))) + ((max (((abs x1) + 1),((abs x2) + 1))) * (r / (2 * (max (((abs x1) + 1),((abs x2) + 1)))))) = (max (((abs x1) + 1),((abs x2) + 1))) * ((r / ((max (((abs x1) + 1),((abs x2) + 1))) * 2)) + (r / ((max (((abs x1) + 1),((abs x2) + 1))) * 2))) .= (r / (max (((abs x1) + 1),((abs x2) + 1)))) * (max (((abs x1) + 1),((abs x2) + 1))) by XCMPLX_1:118 .= r by A20, XCMPLX_1:87 ; hence abs (((f1 (#) f2) . y1) - ((f1 (#) f2) . y2)) < r by A39, A48, XXREAL_0:2; ::_thesis: verum end; hence (f1 (#) f2) | (((X /\ Z) /\ X1) /\ Z1) is uniformly_continuous by Th1; ::_thesis: verum end; theorem Th9: :: FCONT_2:9 for X being set for f being PartFunc of REAL,REAL st X c= dom f & f | X is uniformly_continuous 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 uniformly_continuous holds f | X is continuous let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f & f | X is uniformly_continuous implies f | X is continuous ) assume A1: X c= dom f ; ::_thesis: ( not f | X is uniformly_continuous or f | X is continuous ) assume A2: f | X is uniformly_continuous ; ::_thesis: f | X is continuous now__::_thesis:_for_x0,_r_being_real_number_st_x0_in_X_&_0_<_r_holds_ ex_s_being_real_number_st_ (_0_<_s_&_(_for_x1_being_real_number_st_x1_in_X_&_abs_(x1_-_x0)_<_s_holds_ abs_((f_._x1)_-_(f_._x0))_<_r_)_) let x0, r be real number ; ::_thesis: ( x0 in X & 0 < r implies ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds abs ((f . x1) - (f . x0)) < r ) ) ) assume that A3: x0 in X and A4: 0 < r ; ::_thesis: ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds abs ((f . x1) - (f . x0)) < r ) ) A5: x0 in dom (f | X) by A1, A3, RELAT_1:62; r is Real by XREAL_0:def_1; then consider s being Real such that A6: 0 < s and A7: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < r by A2, A4, Th1; reconsider s = s as real number ; take s = s; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds abs ((f . x1) - (f . x0)) < r ) ) thus 0 < s by A6; ::_thesis: for x1 being real number st x1 in X & abs (x1 - x0) < s holds abs ((f . x1) - (f . x0)) < r let x1 be real number ; ::_thesis: ( x1 in X & abs (x1 - x0) < s implies abs ((f . x1) - (f . x0)) < r ) assume that A8: x1 in X and A9: abs (x1 - x0) < s ; ::_thesis: abs ((f . x1) - (f . x0)) < r x1 in dom (f | X) by A1, A8, RELAT_1:62; hence abs ((f . x1) - (f . x0)) < r by A7, A9, A5; ::_thesis: verum end; hence f | X is continuous by A1, FCONT_1:14; ::_thesis: verum end; theorem Th10: :: FCONT_2:10 for X being set for f being PartFunc of REAL,REAL st f | X is Lipschitzian holds f | X is uniformly_continuous proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f | X is Lipschitzian holds f | X is uniformly_continuous let f be PartFunc of REAL,REAL; ::_thesis: ( f | X is Lipschitzian implies f | X is uniformly_continuous ) assume f | X is Lipschitzian ; ::_thesis: f | X is uniformly_continuous then consider r being real number such that A1: 0 < r and A2: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) by FCONT_1:32; now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_s_being_Element_of_REAL_st_ (_0_<_s_&_(_for_x1,_x2_being_Real_st_x1_in_dom_(f_|_X)_&_x2_in_dom_(f_|_X)_&_abs_(x1_-_x2)_<_s_holds_ abs_((f_._x1)_-_(f_._x2))_<_p_)_) reconsider r = r as Real by XREAL_0:def_1; let p be Real; ::_thesis: ( 0 < p implies ex s being Element of REAL st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < p ) ) ) assume A3: 0 < p ; ::_thesis: ex s being Element of REAL st ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < p ) ) take s = p / r; ::_thesis: ( 0 < s & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < p ) ) thus 0 < s by A1, A3, XREAL_1:139; ::_thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < p let x1, x2 be Real; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) & abs (x1 - x2) < s implies abs ((f . x1) - (f . x2)) < p ) assume that A4: x1 in dom (f | X) and A5: x2 in dom (f | X) and A6: abs (x1 - x2) < s ; ::_thesis: abs ((f . x1) - (f . x2)) < p A7: r * (abs (x1 - x2)) < s * r by A1, A6, XREAL_1:68; abs ((f . x1) - (f . x2)) <= r * (abs (x1 - x2)) by A2, A4, A5; then abs ((f . x1) - (f . x2)) < (p / r) * r by A7, XXREAL_0:2; hence abs ((f . x1) - (f . x2)) < p by A1, XCMPLX_1:87; ::_thesis: verum end; hence f | X is uniformly_continuous by Th1; ::_thesis: verum end; theorem Th11: :: FCONT_2:11 for f being PartFunc of REAL,REAL for Y being Subset of REAL st Y c= dom f & Y is compact & f | Y is continuous holds f | Y is uniformly_continuous proof let f be PartFunc of REAL,REAL; ::_thesis: for Y being Subset of REAL st Y c= dom f & Y is compact & f | Y is continuous holds f | Y is uniformly_continuous let Y be Subset of REAL; ::_thesis: ( Y c= dom f & Y is compact & f | Y is continuous implies f | Y is uniformly_continuous ) assume that A1: Y c= dom f and A2: Y is compact and A3: f | Y is continuous ; ::_thesis: f | Y is uniformly_continuous assume not f | Y is uniformly_continuous ; ::_thesis: contradiction then consider r being Real such that A4: 0 < r and A5: for s being Real st 0 < s holds ex x1, x2 being Real st ( x1 in dom (f | Y) & x2 in dom (f | Y) & abs (x1 - x2) < s & not abs ((f . x1) - (f . x2)) < r ) by Th1; defpred S1[ Element of NAT , Real] means ( $2 in Y & ex x2 being Real st ( x2 in Y & abs ($2 - x2) < 1 / ($1 + 1) & not abs ((f . $2) - (f . x2)) < r ) ); A6: now__::_thesis:_for_n_being_Element_of_NAT_ex_x1_being_Real_st_S1[n,x1] let n be Element of NAT ; ::_thesis: ex x1 being Real st S1[n,x1] consider x1 being Real such that A7: ex x2 being Real st ( x1 in dom (f | Y) & x2 in dom (f | Y) & abs (x1 - x2) < 1 / (n + 1) & not abs ((f . x1) - (f . x2)) < r ) by A5, XREAL_1:139; take x1 = x1; ::_thesis: S1[n,x1] dom (f | Y) = Y by A1, RELAT_1:62; hence S1[n,x1] by A7; ::_thesis: verum end; consider s1 being Real_Sequence such that A8: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A6); now__::_thesis:_for_x_being_set_st_x_in_rng_s1_holds_ x_in_Y let x be set ; ::_thesis: ( x in rng s1 implies x in Y ) assume x in rng s1 ; ::_thesis: x in Y then ex n being Element of NAT st x = s1 . n by FUNCT_2:113; hence x in Y by A8; ::_thesis: verum end; then A9: rng s1 c= Y by TARSKI:def_3; then consider q1 being Real_Sequence such that A10: q1 is subsequence of s1 and A11: q1 is convergent and A12: lim q1 in Y by A2, RCOMP_1:def_3; lim q1 in dom (f | Y) by A1, A12, RELAT_1:57; then A13: f | Y is_continuous_in lim q1 by A3, FCONT_1:def_2; rng q1 c= rng s1 by A10, VALUED_0:21; then A14: rng q1 c= Y by A9, XBOOLE_1:1; then rng q1 c= dom f by A1, XBOOLE_1:1; then rng q1 c= (dom f) /\ Y by A14, XBOOLE_1:19; then A15: rng q1 c= dom (f | Y) by RELAT_1:61; then A16: (f | Y) . (lim q1) = lim ((f | Y) /* q1) by A11, A13, FCONT_1:def_1; A17: (f | Y) /* q1 is convergent by A11, A13, A15, FCONT_1:def_1; defpred S2[ Element of NAT , real number ] means ( $2 in Y & abs ((s1 . $1) - $2) < 1 / ($1 + 1) & not abs ((f . (s1 . $1)) - (f . $2)) < r ); A18: for n being Element of NAT ex x2 being Real st S2[n,x2] by A8; consider s2 being Real_Sequence such that A19: for n being Element of NAT holds S2[n,s2 . n] from FUNCT_2:sch_3(A18); now__::_thesis:_for_x_being_set_st_x_in_rng_s2_holds_ x_in_Y let x be set ; ::_thesis: ( x in rng s2 implies x in Y ) assume x in rng s2 ; ::_thesis: x in Y then ex n being Element of NAT st x = s2 . n by FUNCT_2:113; hence x in Y by A19; ::_thesis: verum end; then A20: rng s2 c= Y by TARSKI:def_3; consider Ns1 being V39() sequence of NAT such that A21: q1 = s1 * Ns1 by A10, VALUED_0:def_17; set q2 = q1 - ((s1 - s2) * Ns1); A22: now__::_thesis:_for_n_being_Element_of_NAT_holds_(q1_-_((s1_-_s2)_*_Ns1))_._n_=_(s2_*_Ns1)_._n let n be Element of NAT ; ::_thesis: (q1 - ((s1 - s2) * Ns1)) . n = (s2 * Ns1) . n thus (q1 - ((s1 - s2) * Ns1)) . n = ((s1 * Ns1) . n) - (((s1 - s2) * Ns1) . n) by A21, RFUNCT_2:1 .= (s1 . (Ns1 . n)) - (((s1 - s2) * Ns1) . n) by FUNCT_2:15 .= (s1 . (Ns1 . n)) - ((s1 - s2) . (Ns1 . n)) by FUNCT_2:15 .= (s1 . (Ns1 . n)) - ((s1 . (Ns1 . n)) - (s2 . (Ns1 . n))) by RFUNCT_2:1 .= (s2 * Ns1) . n by FUNCT_2:15 ; ::_thesis: verum end; then A23: q1 - ((s1 - s2) * Ns1) = s2 * Ns1 by FUNCT_2:63; q1 - ((s1 - s2) * Ns1) is subsequence of s2 by A22, FUNCT_2:63, VALUED_0:def_17; then rng (q1 - ((s1 - s2) * Ns1)) c= rng s2 by VALUED_0:21; then A24: rng (q1 - ((s1 - s2) * Ns1)) c= Y by A20, XBOOLE_1:1; then rng (q1 - ((s1 - s2) * Ns1)) c= dom f by A1, XBOOLE_1:1; then rng (q1 - ((s1 - s2) * Ns1)) c= (dom f) /\ Y by A24, XBOOLE_1:19; then A25: rng (q1 - ((s1 - s2) * Ns1)) c= dom (f | Y) by RELAT_1:61; A26: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ abs_(((s1_-_s2)_._m)_-_0)_<_p let p be real number ; ::_thesis: ( 0 < p implies ex k being Element of NAT st for m being Element of NAT st k <= m holds abs (((s1 - s2) . m) - 0) < p ) assume A27: 0 < p ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds abs (((s1 - s2) . m) - 0) < p consider k being Element of NAT such that A28: p " < k by SEQ_4:3; take k = k; ::_thesis: for m being Element of NAT st k <= m holds abs (((s1 - s2) . m) - 0) < p let m be Element of NAT ; ::_thesis: ( k <= m implies abs (((s1 - s2) . m) - 0) < p ) assume k <= m ; ::_thesis: abs (((s1 - s2) . m) - 0) < p then k + 1 <= m + 1 by XREAL_1:6; then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118; then A29: abs ((s1 . m) - (s2 . m)) < 1 / (k + 1) by A19, XXREAL_0:2; k < k + 1 by NAT_1:13; then p " < k + 1 by A28, XXREAL_0:2; then 1 / (k + 1) < 1 / (p ") by A27, XREAL_1:76; then A30: 1 / (k + 1) < p by XCMPLX_1:216; abs (((s1 - s2) . m) - 0) = abs ((s1 . m) - (s2 . m)) by RFUNCT_2:1; hence abs (((s1 - s2) . m) - 0) < p by A30, A29, XXREAL_0:2; ::_thesis: verum end; then A31: s1 - s2 is convergent by SEQ_2:def_6; A32: (s1 - s2) * Ns1 is subsequence of s1 - s2 by VALUED_0:def_17; then A33: (s1 - s2) * Ns1 is convergent by A31, SEQ_4:16; lim (s1 - s2) = 0 by A26, A31, SEQ_2:def_7; then lim ((s1 - s2) * Ns1) = 0 by A31, A32, SEQ_4:17; then A34: lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - 0 by A11, A33, SEQ_2:12 .= lim q1 ; A35: q1 - ((s1 - s2) * Ns1) is convergent by A11, A33, SEQ_2:11; then A36: (f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent by A13, A34, A25, FCONT_1:def_1; then A37: ((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A17, SEQ_2:11; (f | Y) . (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) by A13, A35, A34, A25, FCONT_1:def_1; then A38: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Y) . (lim q1)) - ((f | Y) . (lim q1)) by A17, A16, A36, SEQ_2:12 .= 0 ; now__::_thesis:_for_n_being_Element_of_NAT_holds_contradiction let n be Element of NAT ; ::_thesis: contradiction consider k being Element of NAT such that A39: for m being Element of NAT st k <= m holds abs (((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . m) - 0) < r by A4, A37, A38, SEQ_2:def_7; A40: q1 . k in rng q1 by VALUED_0:28; A41: (q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1)) by VALUED_0:28; abs (((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - 0) = abs ((((f | Y) /* q1) . k) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)) by RFUNCT_2:1 .= abs (((f | Y) . (q1 . k)) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)) by A15, FUNCT_2:108 .= abs (((f | Y) . (q1 . k)) - ((f | Y) . ((q1 - ((s1 - s2) * Ns1)) . k))) by A25, FUNCT_2:108 .= abs ((f . (q1 . k)) - ((f | Y) . ((q1 - ((s1 - s2) * Ns1)) . k))) by A15, A40, FUNCT_1:47 .= abs ((f . (q1 . k)) - (f . ((q1 - ((s1 - s2) * Ns1)) . k))) by A25, A41, FUNCT_1:47 .= abs ((f . (s1 . (Ns1 . k))) - (f . ((s2 * Ns1) . k))) by A21, A23, FUNCT_2:15 .= abs ((f . (s1 . (Ns1 . k))) - (f . (s2 . (Ns1 . k)))) by FUNCT_2:15 ; hence contradiction by A19, A39; ::_thesis: verum end; hence contradiction ; ::_thesis: verum end; theorem :: FCONT_2:12 for Y being Subset of REAL for f being PartFunc of REAL,REAL st Y c= dom f & Y is compact & f | Y is uniformly_continuous holds f .: Y is compact by Th9, FCONT_1:29; theorem :: FCONT_2:13 for f being PartFunc of REAL,REAL for Y being Subset of REAL st Y <> {} & Y c= dom f & Y is compact & f | Y is uniformly_continuous holds ex x1, x2 being Real st ( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for Y being Subset of REAL st Y <> {} & Y c= dom f & Y is compact & f | Y is uniformly_continuous holds ex x1, x2 being Real st ( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) let Y be Subset of REAL; ::_thesis: ( Y <> {} & Y c= dom f & Y is compact & f | Y is uniformly_continuous implies ex x1, x2 being Real st ( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) ) assume that A1: Y <> {} and A2: Y c= dom f and A3: Y is compact and A4: f | Y is uniformly_continuous ; ::_thesis: ex x1, x2 being Real st ( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) ex x1, x2 being real number st ( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) by A1, A2, A3, A4, Th9, FCONT_1:31; hence ex x1, x2 being Real st ( x1 in Y & x2 in Y & f . x1 = upper_bound (f .: Y) & f . x2 = lower_bound (f .: Y) ) ; ::_thesis: verum end; theorem :: FCONT_2:14 for X being set for f being PartFunc of REAL,REAL st X c= dom f & f | X is V8() holds f | X is uniformly_continuous by Th10; theorem Th15: :: FCONT_2:15 for p, g being Real for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds ex s being Real st ( s in [.p,g.] & r = f . s ) proof let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds ex s being Real st ( s in [.p,g.] & r = f . s ) let f be PartFunc of REAL,REAL; ::_thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds ex s being Real st ( s in [.p,g.] & r = f . s ) ) assume that A1: p <= g and A2: [.p,g.] c= dom f and A3: f | [.p,g.] is continuous ; ::_thesis: for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds ex s being Real st ( s in [.p,g.] & r = f . s ) let r be Real; ::_thesis: ( r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] implies ex s being Real st ( s in [.p,g.] & r = f . s ) ) assume A4: r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] ; ::_thesis: ex s being Real st ( s in [.p,g.] & r = f . s ) A5: [.p,g.] is compact by RCOMP_1:6; A6: ( f . p < f . g implies ex s being Real st ( s in [.p,g.] & r = f . s ) ) proof reconsider f1 = [.p,g.] --> r as Function of [.p,g.],REAL by FUNCOP_1:45; assume that A7: f . p < f . g and A8: for s being Real st s in [.p,g.] holds r <> f . s ; ::_thesis: contradiction [.(f . p),(f . g).] \/ [.(f . g),(f . p).] = [.(f . p),(f . g).] \/ {} by A7, XXREAL_1:29 .= [.(f . p),(f . g).] ; then r in { s where s is Real : ( f . p <= s & s <= f . g ) } by A4, RCOMP_1:def_1; then A9: ex s being Real st ( s = r & f . p <= s & s <= f . g ) ; p in { s where s is Real : ( p <= s & s <= g ) } by A1; then p in [.p,g.] by RCOMP_1:def_1; then A10: r <> f . p by A8; reconsider f1 = f1 as PartFunc of REAL,REAL ; A11: dom f1 = [.p,g.] by FUNCOP_1:13; then A12: [.p,g.] c= (dom f1) /\ (dom f) by A2, XBOOLE_1:19; then A13: [.p,g.] c= dom (f1 - f) by VALUED_1:12; A14: (abs (f1 - f)) " {0} = {} proof assume (abs (f1 - f)) " {0} <> {} ; ::_thesis: contradiction then consider x2 being Real such that A15: x2 in (abs (f1 - f)) " {0} by SUBSET_1:4; x2 in dom (abs (f1 - f)) by A15, FUNCT_1:def_7; then A16: x2 in dom (f1 - f) by VALUED_1:def_11; then x2 in (dom f1) /\ (dom f) by VALUED_1:12; then A17: x2 in [.p,g.] by A11, XBOOLE_0:def_4; (abs (f1 - f)) . x2 in {0} by A15, FUNCT_1:def_7; then (abs (f1 - f)) . x2 = 0 by TARSKI:def_1; then abs ((f1 - f) . x2) = 0 by VALUED_1:18; then (f1 - f) . x2 = 0 by ABSVALUE:2; then (f1 . x2) - (f . x2) = 0 by A16, VALUED_1:13; then r - (f . x2) = 0 by A17, FUNCOP_1:7; hence contradiction by A8, A17; ::_thesis: verum end; A18: dom ((abs (f1 - f)) ^) = (dom (abs (f1 - f))) \ ((abs (f1 - f)) " {0}) by RFUNCT_1:def_2 .= dom (f1 - f) by A14, VALUED_1:def_11 .= [.p,g.] /\ (dom f) by A11, VALUED_1:12 .= [.p,g.] by A2, XBOOLE_1:28 ; for x0 being Real st x0 in [.p,g.] /\ (dom f1) holds f1 . x0 = r by A11, FUNCOP_1:7; then f1 | [.p,g.] is V8() by PARTFUN2:57; then (f1 - f) | [.p,g.] is continuous by A3, A12, FCONT_1:18; then (abs (f1 - f)) | [.p,g.] is continuous by A13, FCONT_1:21; then ((abs (f1 - f)) ^) | [.p,g.] is continuous by A14, FCONT_1:22; then ((abs (f1 - f)) ^) .: [.p,g.] is real-bounded by A5, A18, FCONT_1:29, RCOMP_1:10; then consider M being real number such that A19: M is UpperBound of ((abs (f1 - f)) ^) .: [.p,g.] by XXREAL_2:def_10; A20: for x1 being real number st x1 in ((abs (f1 - f)) ^) .: [.p,g.] holds x1 <= M by A19, XXREAL_2:def_1; 0 + 0 < (abs M) + 1 by COMPLEX1:46, XREAL_1:8; then 0 < ((abs M) + 1) " ; then A21: 0 < 1 / ((abs M) + 1) by XCMPLX_1:215; f | [.p,g.] is uniformly_continuous by A2, A3, Th11, RCOMP_1:6; then consider s being Real such that A22: 0 < s and A23: for x1, x2 being Real st x1 in dom (f | [.p,g.]) & x2 in dom (f | [.p,g.]) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < 1 / ((abs M) + 1) by A21, Th1; A24: now__::_thesis:_for_x1_being_Real_st_x1_in_[.p,g.]_holds_ 1_/_((abs_M)_+_1)_<_abs_(r_-_(f_._x1)) let x1 be Real; ::_thesis: ( x1 in [.p,g.] implies 1 / ((abs M) + 1) < abs (r - (f . x1)) ) assume A25: x1 in [.p,g.] ; ::_thesis: 1 / ((abs M) + 1) < abs (r - (f . x1)) then ((abs (f1 - f)) ^) . x1 in ((abs (f1 - f)) ^) .: [.p,g.] by A18, FUNCT_1:def_6; then ((abs (f1 - f)) ^) . x1 <= M by A20; then ((abs (f1 - f)) . x1) " <= M by A18, A25, RFUNCT_1:def_2; then A26: (abs ((f1 - f) . x1)) " <= M by VALUED_1:18; x1 in (dom f1) /\ (dom f) by A2, A11, A25, XBOOLE_0:def_4; then x1 in dom (f1 - f) by VALUED_1:12; then (abs ((f1 . x1) - (f . x1))) " <= M by A26, VALUED_1:13; then A27: (abs (r - (f . x1))) " <= M by A25, FUNCOP_1:7; r - (f . x1) <> 0 by A8, A25; then A28: 0 < abs (r - (f . x1)) by COMPLEX1:47; M + 0 < (abs M) + 1 by ABSVALUE:4, XREAL_1:8; then (abs (r - (f . x1))) " < (abs M) + 1 by A27, XXREAL_0:2; then 1 / ((abs M) + 1) < 1 / ((abs (r - (f . x1))) ") by A28, XREAL_1:76; hence 1 / ((abs M) + 1) < abs (r - (f . x1)) by XCMPLX_1:216; ::_thesis: verum end; now__::_thesis:_contradiction percases ( p = g or p <> g ) ; suppose p = g ; ::_thesis: contradiction hence contradiction by A7; ::_thesis: verum end; suppose p <> g ; ::_thesis: contradiction then p < g by A1, XXREAL_0:1; then A29: 0 < g - p by XREAL_1:50; then A30: 0 < (g - p) / s by A22, XREAL_1:139; consider k being Element of NAT such that A31: (g - p) / s < k by SEQ_4:3; ((g - p) / s) * s < s * k by A22, A31, XREAL_1:68; then g - p < s * k by A22, XCMPLX_1:87; then (g - p) / k < (s * k) / k by A31, A30, XREAL_1:74; then (g - p) / k < (s * k) * (k ") by XCMPLX_0:def_9; then (g - p) / k < s * (k * (k ")) ; then A32: (g - p) / k < s * 1 by A31, A30, XCMPLX_0:def_7; deffunc H1( Element of NAT ) -> Element of REAL = p + (((g - p) / k) * $1); consider s1 being Real_Sequence such that A33: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1(); A34: 0 < (g - p) / k by A29, A31, A30, XREAL_1:139; A35: now__::_thesis:_for_n_being_Element_of_NAT_st_n_<_k_holds_ (_s1_._n_in_[.p,g.]_&_s1_._(n_+_1)_in_[.p,g.]_&_abs_((f_._(s1_._(n_+_1)))_-_(f_._(s1_._n)))_<_1_/_((abs_M)_+_1)_) let n be Element of NAT ; ::_thesis: ( n < k implies ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) ) ) A36: dom (f | [.p,g.]) = [.p,g.] by A2, RELAT_1:62; assume A37: n < k ; ::_thesis: ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) ) then ((g - p) / k) * n < ((g - p) / k) * k by A34, XREAL_1:68; then ((g - p) / k) * n < g - p by A31, A30, XCMPLX_1:87; then p + (((g - p) / k) * n) < p + (g - p) by XREAL_1:6; then A38: s1 . n < p + (g - p) by A33; n + 1 <= k by A37, NAT_1:13; then ((g - p) / k) * (n + 1) <= ((g - p) / k) * k by A29, XREAL_1:64; then ((g - p) / k) * (n + 1) <= g - p by A31, A30, XCMPLX_1:87; then p + (((g - p) / k) * (n + 1)) <= p + (g - p) by XREAL_1:7; then A39: s1 . (n + 1) <= p + (g - p) by A33; p + 0 <= p + (((g - p) / k) * n) by A29, XREAL_1:7; then p <= s1 . n by A33; then s1 . n in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A38; hence A40: s1 . n in [.p,g.] by RCOMP_1:def_1; ::_thesis: ( s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) ) p + 0 <= p + (((g - p) / k) * (n + 1)) by A29, XREAL_1:7; then p <= s1 . (n + 1) by A33; then s1 . (n + 1) in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A39; hence A41: s1 . (n + 1) in [.p,g.] by RCOMP_1:def_1; ::_thesis: abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) abs ((s1 . (n + 1)) - (s1 . n)) = abs ((p + (((g - p) / k) * (n + 1))) - (s1 . n)) by A33 .= abs ((p + (((g - p) / k) * (n + 1))) - (p + (((g - p) / k) * n))) by A33 .= (g - p) / k by A29, ABSVALUE:def_1 ; hence abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) by A23, A32, A40, A41, A36; ::_thesis: verum end; defpred S1[ Nat] means r <= f . (s1 . $1); A42: s1 . k = p + (((g - p) / k) * k) by A33 .= p + (g - p) by A31, A30, XCMPLX_1:87 .= g ; then A43: ex n being Nat st S1[n] by A9; consider l being Nat such that A44: ( S1[l] & ( for m being Nat st S1[m] holds l <= m ) ) from NAT_1:sch_5(A43); s1 . 0 = p + (((g - p) / k) * 0) by A33 .= p ; then l <> 0 by A9, A10, A44, XXREAL_0:1; then consider l1 being Nat such that A45: l = l1 + 1 by NAT_1:6; reconsider l1 = l1 as Element of NAT by ORDINAL1:def_12; A46: r - (f . (s1 . l1)) <= (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A44, A45, XREAL_1:9; l1 + 1 <= k by A9, A42, A44, A45; then A47: l1 < k by NAT_1:13; then A48: abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) < 1 / ((abs M) + 1) by A35; f . (s1 . l1) < r proof assume r <= f . (s1 . l1) ; ::_thesis: contradiction then l <= l1 by A44; then l + 0 < l by A45, XREAL_1:8; hence contradiction ; ::_thesis: verum end; then A49: 0 < r - (f . (s1 . l1)) by XREAL_1:50; then 0 < (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A44, A45, XREAL_1:9; then abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) = (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by ABSVALUE:def_1; then A50: abs (r - (f . (s1 . l1))) <= abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) by A49, A46, ABSVALUE:def_1; s1 . l1 in [.p,g.] by A35, A47; hence contradiction by A24, A50, A48, XXREAL_0:2; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; A51: ( f . g < f . p implies ex s being Real st ( s in [.p,g.] & r = f . s ) ) proof reconsider f1 = [.p,g.] --> r as Function of [.p,g.],REAL by FUNCOP_1:45; assume that A52: f . g < f . p and A53: for s being Real st s in [.p,g.] holds r <> f . s ; ::_thesis: contradiction [.(f . p),(f . g).] \/ [.(f . g),(f . p).] = {} \/ [.(f . g),(f . p).] by A52, XXREAL_1:29 .= [.(f . g),(f . p).] ; then r in { s where s is Real : ( f . g <= s & s <= f . p ) } by A4, RCOMP_1:def_1; then A54: ex s being Real st ( s = r & f . g <= s & s <= f . p ) ; g in { s where s is Real : ( p <= s & s <= g ) } by A1; then g in [.p,g.] by RCOMP_1:def_1; then A55: r <> f . g by A53; reconsider f1 = f1 as PartFunc of REAL,REAL ; A56: dom f1 = [.p,g.] by FUNCOP_1:13; then A57: [.p,g.] c= (dom f1) /\ (dom f) by A2, XBOOLE_1:19; then A58: [.p,g.] c= dom (f1 - f) by VALUED_1:12; A59: (abs (f1 - f)) " {0} = {} proof assume (abs (f1 - f)) " {0} <> {} ; ::_thesis: contradiction then consider x2 being Real such that A60: x2 in (abs (f1 - f)) " {0} by SUBSET_1:4; x2 in dom (abs (f1 - f)) by A60, FUNCT_1:def_7; then A61: x2 in dom (f1 - f) by VALUED_1:def_11; then x2 in (dom f1) /\ (dom f) by VALUED_1:12; then A62: x2 in [.p,g.] by A56, XBOOLE_0:def_4; (abs (f1 - f)) . x2 in {0} by A60, FUNCT_1:def_7; then (abs (f1 - f)) . x2 = 0 by TARSKI:def_1; then abs ((f1 - f) . x2) = 0 by VALUED_1:18; then (f1 - f) . x2 = 0 by ABSVALUE:2; then (f1 . x2) - (f . x2) = 0 by A61, VALUED_1:13; then r - (f . x2) = 0 by A62, FUNCOP_1:7; hence contradiction by A53, A62; ::_thesis: verum end; A63: dom ((abs (f1 - f)) ^) = (dom (abs (f1 - f))) \ ((abs (f1 - f)) " {0}) by RFUNCT_1:def_2 .= dom (f1 - f) by A59, VALUED_1:def_11 .= [.p,g.] /\ (dom f) by A56, VALUED_1:12 .= [.p,g.] by A2, XBOOLE_1:28 ; for x0 being Real st x0 in [.p,g.] /\ (dom f1) holds f1 . x0 = r by A56, FUNCOP_1:7; then f1 | [.p,g.] is V8() by PARTFUN2:57; then (f1 - f) | [.p,g.] is continuous by A3, A57, FCONT_1:18; then (abs (f1 - f)) | [.p,g.] is continuous by A58, FCONT_1:21; then ((abs (f1 - f)) ^) | [.p,g.] is continuous by A59, FCONT_1:22; then ((abs (f1 - f)) ^) .: [.p,g.] is real-bounded by A5, A63, FCONT_1:29, RCOMP_1:10; then consider M being real number such that A64: M is UpperBound of ((abs (f1 - f)) ^) .: [.p,g.] by XXREAL_2:def_10; A65: for x1 being real number st x1 in ((abs (f1 - f)) ^) .: [.p,g.] holds x1 <= M by A64, XXREAL_2:def_1; 0 + 0 < (abs M) + 1 by COMPLEX1:46, XREAL_1:8; then 0 < ((abs M) + 1) " ; then A66: 0 < 1 / ((abs M) + 1) by XCMPLX_1:215; f | [.p,g.] is uniformly_continuous by A2, A3, Th11, RCOMP_1:6; then consider s being Real such that A67: 0 < s and A68: for x1, x2 being Real st x1 in dom (f | [.p,g.]) & x2 in dom (f | [.p,g.]) & abs (x1 - x2) < s holds abs ((f . x1) - (f . x2)) < 1 / ((abs M) + 1) by A66, Th1; A69: now__::_thesis:_for_x1_being_Real_st_x1_in_[.p,g.]_holds_ 1_/_((abs_M)_+_1)_<_abs_(r_-_(f_._x1)) let x1 be Real; ::_thesis: ( x1 in [.p,g.] implies 1 / ((abs M) + 1) < abs (r - (f . x1)) ) assume A70: x1 in [.p,g.] ; ::_thesis: 1 / ((abs M) + 1) < abs (r - (f . x1)) then ((abs (f1 - f)) ^) . x1 in ((abs (f1 - f)) ^) .: [.p,g.] by A63, FUNCT_1:def_6; then ((abs (f1 - f)) ^) . x1 <= M by A65; then ((abs (f1 - f)) . x1) " <= M by A63, A70, RFUNCT_1:def_2; then A71: (abs ((f1 - f) . x1)) " <= M by VALUED_1:18; x1 in (dom f1) /\ (dom f) by A2, A56, A70, XBOOLE_0:def_4; then x1 in dom (f1 - f) by VALUED_1:12; then (abs ((f1 . x1) - (f . x1))) " <= M by A71, VALUED_1:13; then A72: (abs (r - (f . x1))) " <= M by A70, FUNCOP_1:7; r - (f . x1) <> 0 by A53, A70; then A73: 0 < abs (r - (f . x1)) by COMPLEX1:47; M + 0 < (abs M) + 1 by ABSVALUE:4, XREAL_1:8; then (abs (r - (f . x1))) " < (abs M) + 1 by A72, XXREAL_0:2; then 1 / ((abs M) + 1) < 1 / ((abs (r - (f . x1))) ") by A73, XREAL_1:76; hence 1 / ((abs M) + 1) < abs (r - (f . x1)) by XCMPLX_1:216; ::_thesis: verum end; now__::_thesis:_contradiction percases ( p = g or p <> g ) ; suppose p = g ; ::_thesis: contradiction hence contradiction by A52; ::_thesis: verum end; suppose p <> g ; ::_thesis: contradiction then p < g by A1, XXREAL_0:1; then A74: 0 < g - p by XREAL_1:50; then A75: 0 < (g - p) / s by A67, XREAL_1:139; consider k being Element of NAT such that A76: (g - p) / s < k by SEQ_4:3; ((g - p) / s) * s < s * k by A67, A76, XREAL_1:68; then g - p < s * k by A67, XCMPLX_1:87; then (g - p) / k < (s * k) / k by A76, A75, XREAL_1:74; then (g - p) / k < (s * k) * (k ") by XCMPLX_0:def_9; then (g - p) / k < s * (k * (k ")) ; then A77: (g - p) / k < s * 1 by A76, A75, XCMPLX_0:def_7; deffunc H1( Element of NAT ) -> Element of REAL = g - (((g - p) / k) * $1); consider s1 being Real_Sequence such that A78: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1(); A79: 0 < (g - p) / k by A74, A76, A75, XREAL_1:139; A80: now__::_thesis:_for_n_being_Element_of_NAT_st_n_<_k_holds_ (_s1_._n_in_[.p,g.]_&_s1_._(n_+_1)_in_[.p,g.]_&_abs_((f_._(s1_._(n_+_1)))_-_(f_._(s1_._n)))_<_1_/_((abs_M)_+_1)_) let n be Element of NAT ; ::_thesis: ( n < k implies ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) ) ) A81: dom (f | [.p,g.]) = [.p,g.] by A2, RELAT_1:62; assume A82: n < k ; ::_thesis: ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) ) then ((g - p) / k) * n < ((g - p) / k) * k by A79, XREAL_1:68; then ((g - p) / k) * n < g - p by A76, A75, XCMPLX_1:87; then g - (g - p) < g - (((g - p) / k) * n) by XREAL_1:15; then A83: g - (g - p) < s1 . n by A78; n + 1 <= k by A82, NAT_1:13; then ((g - p) / k) * (n + 1) <= ((g - p) / k) * k by A74, XREAL_1:64; then ((g - p) / k) * (n + 1) <= g - p by A76, A75, XCMPLX_1:87; then g - (g - p) <= g - (((g - p) / k) * (n + 1)) by XREAL_1:13; then A84: g - (g - p) <= s1 . (n + 1) by A78; g - (((g - p) / k) * n) <= g - 0 by A74, XREAL_1:13; then s1 . n <= g by A78; then s1 . n in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A83; hence A85: s1 . n in [.p,g.] by RCOMP_1:def_1; ::_thesis: ( s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) ) g - (((g - p) / k) * (n + 1)) <= g - 0 by A74, XREAL_1:13; then s1 . (n + 1) <= g by A78; then s1 . (n + 1) in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A84; hence A86: s1 . (n + 1) in [.p,g.] by RCOMP_1:def_1; ::_thesis: abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) abs ((s1 . (n + 1)) - (s1 . n)) = abs ((g - (((g - p) / k) * (n + 1))) - (s1 . n)) by A78 .= abs ((g - (((g - p) / k) * (n + 1))) - (g - (((g - p) / k) * n))) by A78 .= abs (- ((((g - p) / k) * (n + 1)) - (((g - p) / k) * n))) .= abs (((g - p) / k) * ((n + 1) - n)) by COMPLEX1:52 .= (g - p) / k by A74, ABSVALUE:def_1 ; hence abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) by A68, A77, A85, A86, A81; ::_thesis: verum end; defpred S1[ Nat] means r <= f . (s1 . $1); A87: s1 . k = g - (((g - p) / k) * k) by A78 .= g - (g - p) by A76, A75, XCMPLX_1:87 .= p ; then A88: ex n being Nat st S1[n] by A54; consider l being Nat such that A89: ( S1[l] & ( for m being Nat st S1[m] holds l <= m ) ) from NAT_1:sch_5(A88); s1 . 0 = g - (((g - p) / k) * 0) by A78 .= g ; then l <> 0 by A54, A55, A89, XXREAL_0:1; then consider l1 being Nat such that A90: l = l1 + 1 by NAT_1:6; reconsider l1 = l1 as Element of NAT by ORDINAL1:def_12; A91: r - (f . (s1 . l1)) <= (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A89, A90, XREAL_1:9; l1 + 1 <= k by A54, A87, A89, A90; then A92: l1 < k by NAT_1:13; then A93: abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) < 1 / ((abs M) + 1) by A80; f . (s1 . l1) < r proof assume r <= f . (s1 . l1) ; ::_thesis: contradiction then l <= l1 by A89; then l + 0 < l by A90, XREAL_1:8; hence contradiction ; ::_thesis: verum end; then A94: 0 < r - (f . (s1 . l1)) by XREAL_1:50; then 0 < (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A89, A90, XREAL_1:9; then abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) = (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by ABSVALUE:def_1; then A95: abs (r - (f . (s1 . l1))) <= abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) by A94, A91, ABSVALUE:def_1; s1 . l1 in [.p,g.] by A80, A92; hence contradiction by A69, A95, A93, XXREAL_0:2; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; ( f . p = f . g implies ex s being Real st ( s in [.p,g.] & r = f . s ) ) proof assume A96: f . p = f . g ; ::_thesis: ex s being Real st ( s in [.p,g.] & r = f . s ) take p ; ::_thesis: ( p in [.p,g.] & r = f . p ) thus p in [.p,g.] by A1, XXREAL_1:1; ::_thesis: r = f . p [.(f . p),(f . g).] \/ [.(f . g),(f . p).] = {(f . p)} by A96, XXREAL_1:17; hence r = f . p by A4, TARSKI:def_1; ::_thesis: verum end; hence ex s being Real st ( s in [.p,g.] & r = f . s ) by A6, A51, XXREAL_0:1; ::_thesis: verum end; theorem Th16: :: FCONT_2:16 for p, g being Real for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds ex s being Real st ( s in [.p,g.] & r = f . s ) proof let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds ex s being Real st ( s in [.p,g.] & r = f . s ) let f be PartFunc of REAL,REAL; ::_thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds ex s being Real st ( s in [.p,g.] & r = f . s ) ) assume that A1: p <= g and A2: [.p,g.] c= dom f and A3: f | [.p,g.] is continuous ; ::_thesis: for r being Real st r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] holds ex s being Real st ( s in [.p,g.] & r = f . s ) [.p,g.] is compact by RCOMP_1:6; then A4: f .: [.p,g.] is real-bounded by A2, A3, FCONT_1:29, RCOMP_1:10; set ub = upper_bound (f .: [.p,g.]); set lb = lower_bound (f .: [.p,g.]); [.p,g.] <> {} by A1, XXREAL_1:1; then consider x2, x1 being real number such that A5: x2 in [.p,g.] and A6: x1 in [.p,g.] and A7: f . x2 = upper_bound (f .: [.p,g.]) and A8: f . x1 = lower_bound (f .: [.p,g.]) by A2, A3, FCONT_1:31, RCOMP_1:6; reconsider x1 = x1, x2 = x2 as Real by XREAL_0:def_1; let r be Real; ::_thesis: ( r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] implies ex s being Real st ( s in [.p,g.] & r = f . s ) ) assume A9: r in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ; ::_thesis: ex s being Real st ( s in [.p,g.] & r = f . s ) f . x1 in f .: [.p,g.] by A2, A6, FUNCT_1:def_6; then A10: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] \/ [.(upper_bound (f .: [.p,g.])),(lower_bound (f .: [.p,g.])).] by A4, SEQ_4:11, XXREAL_1:222; now__::_thesis:_ex_s_being_Real_st_ (_s_in_[.p,g.]_&_r_=_f_._s_) percases ( x1 <= x2 or x2 <= x1 ) ; supposeA11: x1 <= x2 ; ::_thesis: ex s being Real st ( s in [.p,g.] & r = f . s ) A12: [.x1,x2.] c= [.p,g.] by A5, A6, XXREAL_2:def_12; A13: [.x1,x2.] c= [.p,g.] by A5, A6, XXREAL_2:def_12; then f | [.x1,x2.] is continuous by A3, FCONT_1:16; then consider s being Real such that A14: s in [.x1,x2.] and A15: r = f . s by A2, A9, A7, A8, A10, A11, A12, Th15, XBOOLE_1:1; take s = s; ::_thesis: ( s in [.p,g.] & r = f . s ) thus ( s in [.p,g.] & r = f . s ) by A13, A14, A15; ::_thesis: verum end; supposeA16: x2 <= x1 ; ::_thesis: ex s being Real st ( s in [.p,g.] & r = f . s ) A17: [.x2,x1.] c= [.p,g.] by A5, A6, XXREAL_2:def_12; A18: [.x2,x1.] c= [.p,g.] by A5, A6, XXREAL_2:def_12; then f | [.x2,x1.] is continuous by A3, FCONT_1:16; then consider s being Real such that A19: s in [.x2,x1.] and A20: r = f . s by A2, A9, A7, A8, A10, A16, A17, Th15, XBOOLE_1:1; take s = s; ::_thesis: ( s in [.p,g.] & r = f . s ) thus ( s in [.p,g.] & r = f . s ) by A18, A19, A20; ::_thesis: verum end; end; end; hence ex s being Real st ( s in [.p,g.] & r = f . s ) ; ::_thesis: verum end; theorem Th17: :: FCONT_2:17 for p, g being Real for f being PartFunc of REAL,REAL st f is one-to-one & [.p,g.] c= dom f & p <= g & f | [.p,g.] is continuous & not f | [.p,g.] is increasing holds f | [.p,g.] is decreasing proof let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st f is one-to-one & [.p,g.] c= dom f & p <= g & f | [.p,g.] is continuous & not f | [.p,g.] is increasing holds f | [.p,g.] is decreasing let f be PartFunc of REAL,REAL; ::_thesis: ( f is one-to-one & [.p,g.] c= dom f & p <= g & f | [.p,g.] is continuous & not f | [.p,g.] is increasing implies f | [.p,g.] is decreasing ) assume that A1: f is one-to-one and A2: [.p,g.] c= dom f and A3: p <= g and A4: f | [.p,g.] is continuous and A5: not f | [.p,g.] is increasing and A6: not f | [.p,g.] is decreasing ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( p = g or p <> g ) ; suppose p = g ; ::_thesis: contradiction then [.p,g.] = {p} by XXREAL_1:17; hence contradiction by A6, RFUNCT_2:44; ::_thesis: verum end; supposeA7: p <> g ; ::_thesis: contradiction A8: g in [.p,g.] by A3, XXREAL_1:1; A9: p in [.p,g.] by A3, XXREAL_1:1; then A10: f . p <> f . g by A1, A2, A7, A8, FUNCT_1:def_4; now__::_thesis:_contradiction percases ( f . p < f . g or f . p > f . g ) by A10, XXREAL_0:1; supposeA11: f . p < f . g ; ::_thesis: contradiction A12: for x1 being Real st p <= x1 & x1 <= g holds ( f . p <= f . x1 & f . x1 <= f . g ) proof let x1 be Real; ::_thesis: ( p <= x1 & x1 <= g implies ( f . p <= f . x1 & f . x1 <= f . g ) ) assume that A13: p <= x1 and A14: x1 <= g and A15: ( not f . p <= f . x1 or not f . x1 <= f . g ) ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( f . x1 < f . p or f . g < f . x1 ) by A15; supposeA16: f . x1 < f . p ; ::_thesis: contradiction then f . p in { r where r is Real : ( f . x1 <= r & r <= f . g ) } by A11; then f . p in [.(f . x1),(f . g).] by RCOMP_1:def_1; then A17: f . p in [.(f . x1),(f . g).] \/ [.(f . g),(f . x1).] by XBOOLE_0:def_3; x1 in { r where r is Real : ( p <= r & r <= g ) } by A13, A14; then A18: x1 in [.p,g.] by RCOMP_1:def_1; g in [.p,g.] by A3, XXREAL_1:1; then A19: [.x1,g.] c= [.p,g.] by A18, XXREAL_2:def_12; then f | [.x1,g.] is continuous by A4, FCONT_1:16; then consider s being Real such that A20: s in [.x1,g.] and A21: f . s = f . p by A2, A14, A19, A17, Th15, XBOOLE_1:1; s in { t where t is Real : ( x1 <= t & t <= g ) } by A20, RCOMP_1:def_1; then A22: ex r being Real st ( r = s & x1 <= r & r <= g ) ; A23: x1 > p by A13, A16, XXREAL_0:1; s in [.p,g.] by A19, A20; hence contradiction by A1, A2, A9, A23, A21, A22, FUNCT_1:def_4; ::_thesis: verum end; supposeA24: f . g < f . x1 ; ::_thesis: contradiction then f . g in { r where r is Real : ( f . p <= r & r <= f . x1 ) } by A11; then f . g in [.(f . p),(f . x1).] by RCOMP_1:def_1; then A25: f . g in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def_3; x1 in { r where r is Real : ( p <= r & r <= g ) } by A13, A14; then A26: x1 in [.p,g.] by RCOMP_1:def_1; p in [.p,g.] by A3, XXREAL_1:1; then A27: [.p,x1.] c= [.p,g.] by A26, XXREAL_2:def_12; then f | [.p,x1.] is continuous by A4, FCONT_1:16; then consider s being Real such that A28: s in [.p,x1.] and A29: f . s = f . g by A2, A13, A27, A25, Th15, XBOOLE_1:1; s in { t where t is Real : ( p <= t & t <= x1 ) } by A28, RCOMP_1:def_1; then A30: ex r being Real st ( r = s & p <= r & r <= x1 ) ; s in [.p,g.] by A27, A28; then s = g by A1, A2, A8, A29, FUNCT_1:def_4; hence contradiction by A14, A24, A30, XXREAL_0:1; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; consider x1, x2 being Real such that A31: x1 in [.p,g.] /\ (dom f) and A32: x2 in [.p,g.] /\ (dom f) and A33: x1 < x2 and A34: f . x2 <= f . x1 by A5, RFUNCT_2:20; A35: x1 in [.p,g.] by A31, XBOOLE_0:def_4; then A36: [.p,x1.] c= [.p,g.] by A9, XXREAL_2:def_12; A37: x2 in [.p,g.] by A32, XBOOLE_0:def_4; then x2 in { r where r is Real : ( p <= r & r <= g ) } by RCOMP_1:def_1; then ex r being Real st ( r = x2 & p <= r & r <= g ) ; then f . p <= f . x2 by A12; then f . x2 in { r where r is Real : ( f . p <= r & r <= f . x1 ) } by A34; then f . x2 in [.(f . p),(f . x1).] by RCOMP_1:def_1; then A38: f . x2 in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def_3; x1 in { t where t is Real : ( p <= t & t <= g ) } by A35, RCOMP_1:def_1; then A39: ex r being Real st ( r = x1 & p <= r & r <= g ) ; p in [.p,g.] by A3, XXREAL_1:1; then A40: [.p,x1.] c= [.p,g.] by A35, XXREAL_2:def_12; then f | [.p,x1.] is continuous by A4, FCONT_1:16; then consider s being Real such that A41: s in [.p,x1.] and A42: f . s = f . x2 by A2, A39, A38, A36, Th15, XBOOLE_1:1; s in { t where t is Real : ( p <= t & t <= x1 ) } by A41, RCOMP_1:def_1; then A43: ex r being Real st ( r = s & p <= r & r <= x1 ) ; s in [.p,g.] by A40, A41; hence contradiction by A1, A2, A33, A37, A42, A43, FUNCT_1:def_4; ::_thesis: verum end; supposeA44: f . p > f . g ; ::_thesis: contradiction A45: for x1 being Real st p <= x1 & x1 <= g holds ( f . g <= f . x1 & f . x1 <= f . p ) proof let x1 be Real; ::_thesis: ( p <= x1 & x1 <= g implies ( f . g <= f . x1 & f . x1 <= f . p ) ) assume that A46: p <= x1 and A47: x1 <= g and A48: ( not f . g <= f . x1 or not f . x1 <= f . p ) ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( f . x1 < f . g or f . p < f . x1 ) by A48; supposeA49: f . x1 < f . g ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( g = x1 or g <> x1 ) ; suppose g = x1 ; ::_thesis: contradiction hence contradiction by A49; ::_thesis: verum end; supposeA50: g <> x1 ; ::_thesis: contradiction x1 in { r where r is Real : ( p <= r & r <= g ) } by A46, A47; then A51: x1 in [.p,g.] by RCOMP_1:def_1; f . g in { r where r is Real : ( f . x1 <= r & r <= f . p ) } by A44, A49; then f . g in [.(f . x1),(f . p).] by RCOMP_1:def_1; then A52: f . g in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def_3; p in [.p,g.] by A3, XXREAL_1:1; then A53: [.p,x1.] c= [.p,g.] by A51, XXREAL_2:def_12; then f | [.p,x1.] is continuous by A4, FCONT_1:16; then consider s being Real such that A54: s in [.p,x1.] and A55: f . s = f . g by A2, A46, A53, A52, Th15, XBOOLE_1:1; s in { t where t is Real : ( p <= t & t <= x1 ) } by A54, RCOMP_1:def_1; then A56: ex r being Real st ( r = s & p <= r & r <= x1 ) ; s in [.p,g.] by A53, A54; then s = g by A1, A2, A8, A55, FUNCT_1:def_4; hence contradiction by A47, A50, A56, XXREAL_0:1; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposeA57: f . p < f . x1 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( p = x1 or p <> x1 ) ; suppose p = x1 ; ::_thesis: contradiction hence contradiction by A57; ::_thesis: verum end; supposeA58: p <> x1 ; ::_thesis: contradiction x1 in { r where r is Real : ( p <= r & r <= g ) } by A46, A47; then A59: x1 in [.p,g.] by RCOMP_1:def_1; f . p in { r where r is Real : ( f . g <= r & r <= f . x1 ) } by A44, A57; then f . p in [.(f . g),(f . x1).] by RCOMP_1:def_1; then A60: f . p in [.(f . x1),(f . g).] \/ [.(f . g),(f . x1).] by XBOOLE_0:def_3; g in [.p,g.] by A3, XXREAL_1:1; then A61: [.x1,g.] c= [.p,g.] by A59, XXREAL_2:def_12; then f | [.x1,g.] is continuous by A4, FCONT_1:16; then consider s being Real such that A62: s in [.x1,g.] and A63: f . s = f . p by A2, A47, A61, A60, Th15, XBOOLE_1:1; s in { t where t is Real : ( x1 <= t & t <= g ) } by A62, RCOMP_1:def_1; then A64: ex r being Real st ( r = s & x1 <= r & r <= g ) ; s in [.p,g.] by A61, A62; then s = p by A1, A2, A9, A63, FUNCT_1:def_4; hence contradiction by A46, A58, A64, XXREAL_0:1; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; consider x1, x2 being Real such that A65: x1 in [.p,g.] /\ (dom f) and A66: x2 in [.p,g.] /\ (dom f) and A67: x1 < x2 and A68: f . x1 <= f . x2 by A6, RFUNCT_2:21; A69: x2 in [.p,g.] by A66, XBOOLE_0:def_4; then A70: [.x2,g.] c= [.p,g.] by A8, XXREAL_2:def_12; A71: x1 in [.p,g.] by A65, XBOOLE_0:def_4; then x1 in { t where t is Real : ( p <= t & t <= g ) } by RCOMP_1:def_1; then ex r being Real st ( r = x1 & p <= r & r <= g ) ; then f . g <= f . x1 by A45; then f . x1 in { r where r is Real : ( f . g <= r & r <= f . x2 ) } by A68; then f . x1 in [.(f . g),(f . x2).] by RCOMP_1:def_1; then A72: f . x1 in [.(f . x2),(f . g).] \/ [.(f . g),(f . x2).] by XBOOLE_0:def_3; x2 in { r where r is Real : ( p <= r & r <= g ) } by A69, RCOMP_1:def_1; then A73: ex r being Real st ( r = x2 & p <= r & r <= g ) ; g in [.p,g.] by A3, XXREAL_1:1; then A74: [.x2,g.] c= [.p,g.] by A69, XXREAL_2:def_12; then f | [.x2,g.] is continuous by A4, FCONT_1:16; then consider s being Real such that A75: s in [.x2,g.] and A76: f . s = f . x1 by A2, A73, A72, A70, Th15, XBOOLE_1:1; s in { t where t is Real : ( x2 <= t & t <= g ) } by A75, RCOMP_1:def_1; then A77: ex r being Real st ( r = s & x2 <= r & r <= g ) ; s in [.p,g.] by A74, A75; hence contradiction by A1, A2, A67, A71, A76, A77, FUNCT_1:def_4; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem :: FCONT_2:18 for p, g being Real for f being PartFunc of REAL,REAL st f is one-to-one & p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous & not ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) holds ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) proof let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st f is one-to-one & p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous & not ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) holds ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) let f be PartFunc of REAL,REAL; ::_thesis: ( f is one-to-one & p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous & not ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) implies ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) ) assume that A1: f is one-to-one and A2: p <= g and A3: [.p,g.] c= dom f and A4: f | [.p,g.] is continuous ; ::_thesis: ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) ) A5: p in [.p,g.] by A2, XXREAL_1:1; then A6: f . p in f .: [.p,g.] by A3, FUNCT_1:def_6; A7: g in [.p,g.] by A2, XXREAL_1:1; then A8: f . g in f .: [.p,g.] by A3, FUNCT_1:def_6; A9: g in [.p,g.] /\ (dom f) by A3, A7, XBOOLE_0:def_4; A10: p in [.p,g.] /\ (dom f) by A3, A5, XBOOLE_0:def_4; [.p,g.] <> {} by A2, XXREAL_1:1; then consider x1, x2 being real number such that A11: x1 in [.p,g.] and A12: x2 in [.p,g.] and A13: f . x1 = upper_bound (f .: [.p,g.]) and A14: f . x2 = lower_bound (f .: [.p,g.]) by A3, A4, FCONT_1:31, RCOMP_1:6; A15: x2 in [.p,g.] /\ (dom f) by A3, A12, XBOOLE_0:def_4; x2 in { t where t is Real : ( p <= t & t <= g ) } by A12, RCOMP_1:def_1; then A16: ex r being Real st ( r = x2 & p <= r & r <= g ) ; x1 in { r where r is Real : ( p <= r & r <= g ) } by A11, RCOMP_1:def_1; then A17: ex r being Real st ( r = x1 & p <= r & r <= g ) ; [.p,g.] is compact by RCOMP_1:6; then A18: f .: [.p,g.] is real-bounded by A3, A4, FCONT_1:29, RCOMP_1:10; A19: x1 in [.p,g.] /\ (dom f) by A3, A11, XBOOLE_0:def_4; now__::_thesis:_(_(_lower_bound_(f_.:_[.p,g.])_=_f_._p_&_upper_bound_(f_.:_[.p,g.])_=_f_._g_)_or_(_lower_bound_(f_.:_[.p,g.])_=_f_._g_&_upper_bound_(f_.:_[.p,g.])_=_f_._p_)_) percases ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) by A1, A2, A3, A4, Th17; supposeA20: f | [.p,g.] is increasing ; ::_thesis: ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) ) A21: now__::_thesis:_not_x1_<>_g assume x1 <> g ; ::_thesis: contradiction then x1 < g by A17, XXREAL_0:1; then f . x1 < f . g by A9, A19, A20, RFUNCT_2:20; hence contradiction by A8, A18, A13, SEQ_4:def_1; ::_thesis: verum end; now__::_thesis:_not_x2_<>_p assume x2 <> p ; ::_thesis: contradiction then p < x2 by A16, XXREAL_0:1; then f . p < f . x2 by A10, A15, A20, RFUNCT_2:20; hence contradiction by A6, A18, A14, SEQ_4:def_2; ::_thesis: verum end; hence ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) ) by A13, A14, A21; ::_thesis: verum end; supposeA22: f | [.p,g.] is decreasing ; ::_thesis: ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) ) A23: now__::_thesis:_not_x2_<>_g assume x2 <> g ; ::_thesis: contradiction then x2 < g by A16, XXREAL_0:1; then f . g < f . x2 by A9, A15, A22, RFUNCT_2:21; hence contradiction by A8, A18, A14, SEQ_4:def_2; ::_thesis: verum end; now__::_thesis:_not_x1_<>_p assume x1 <> p ; ::_thesis: contradiction then p < x1 by A17, XXREAL_0:1; then f . x1 < f . p by A10, A19, A22, RFUNCT_2:21; hence contradiction by A6, A18, A13, SEQ_4:def_1; ::_thesis: verum end; hence ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) ) by A13, A14, A23; ::_thesis: verum end; end; end; hence ( ( lower_bound (f .: [.p,g.]) = f . p & upper_bound (f .: [.p,g.]) = f . g ) or ( lower_bound (f .: [.p,g.]) = f . g & upper_bound (f .: [.p,g.]) = f . p ) ) ; ::_thesis: verum end; theorem Th19: :: FCONT_2:19 for p, g being Real for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] proof let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] let f be PartFunc of REAL,REAL; ::_thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ) assume that A1: p <= g and A2: [.p,g.] c= dom f and A3: f | [.p,g.] is continuous ; ::_thesis: f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] [.p,g.] is compact by RCOMP_1:6; then A4: f .: [.p,g.] is real-bounded by A2, A3, FCONT_1:29, RCOMP_1:10; now__::_thesis:_for_y_being_Real_holds_ (_(_y_in_f_.:_[.p,g.]_implies_y_in_[.(lower_bound_(f_.:_[.p,g.])),(upper_bound_(f_.:_[.p,g.])).]_)_&_(_y_in_[.(lower_bound_(f_.:_[.p,g.])),(upper_bound_(f_.:_[.p,g.])).]_implies_y_in_f_.:_[.p,g.]_)_) let y be Real; ::_thesis: ( ( y in f .: [.p,g.] implies y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ) & ( y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] implies y in f .: [.p,g.] ) ) thus ( y in f .: [.p,g.] implies y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ) ::_thesis: ( y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] implies y in f .: [.p,g.] ) proof assume A5: y in f .: [.p,g.] ; ::_thesis: y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] then A6: y >= lower_bound (f .: [.p,g.]) by A4, SEQ_4:def_2; y <= upper_bound (f .: [.p,g.]) by A4, A5, SEQ_4:def_1; then y in { s where s is Real : ( lower_bound (f .: [.p,g.]) <= s & s <= upper_bound (f .: [.p,g.]) ) } by A6; hence y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] by RCOMP_1:def_1; ::_thesis: verum end; assume y in [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] ; ::_thesis: y in f .: [.p,g.] then ex x0 being Real st ( x0 in [.p,g.] & y = f . x0 ) by A1, A2, A3, Th16; hence y in f .: [.p,g.] by A2, FUNCT_1:def_6; ::_thesis: verum end; hence f .: [.p,g.] = [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] by SUBSET_1:3; ::_thesis: verum end; theorem :: FCONT_2:20 for p, g being Real for f being one-to-one PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous proof let p, g be Real; ::_thesis: for f being one-to-one PartFunc of REAL,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous let f be one-to-one PartFunc of REAL,REAL; ::_thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous ) assume that A1: p <= g and A2: [.p,g.] c= dom f and A3: f | [.p,g.] is continuous ; ::_thesis: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous now__::_thesis:_(f_")_|_[.(lower_bound_(f_.:_[.p,g.])),(upper_bound_(f_.:_[.p,g.])).]_is_continuous percases ( f | [.p,g.] is increasing or f | [.p,g.] is decreasing ) by A1, A2, A3, Th17; suppose f | [.p,g.] is increasing ; ::_thesis: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous then ((f | [.p,g.]) ") | (f .: [.p,g.]) is increasing by RFUNCT_2:51; then ((f ") | (f .: [.p,g.])) | (f .: [.p,g.]) is increasing by RFUNCT_2:17; then (f ") | (f .: [.p,g.]) is monotone by RELAT_1:72; then A4: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is monotone by A1, A2, A3, Th19; (f ") .: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = (f ") .: (f .: [.p,g.]) by A1, A2, A3, Th19 .= ((f ") | (f .: [.p,g.])) .: (f .: [.p,g.]) by RELAT_1:129 .= ((f | [.p,g.]) ") .: (f .: [.p,g.]) by RFUNCT_2:17 .= ((f | [.p,g.]) ") .: (rng (f | [.p,g.])) by RELAT_1:115 .= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33 .= rng ((f | [.p,g.]) ") by RELAT_1:113 .= dom (f | [.p,g.]) by FUNCT_1:33 .= (dom f) /\ [.p,g.] by RELAT_1:61 .= [.p,g.] by A2, XBOOLE_1:28 ; hence (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous by A1, A4, FCONT_1:46; ::_thesis: verum end; suppose f | [.p,g.] is decreasing ; ::_thesis: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous then ((f | [.p,g.]) ") | (f .: [.p,g.]) is decreasing by RFUNCT_2:52; then ((f ") | (f .: [.p,g.])) | (f .: [.p,g.]) is decreasing by RFUNCT_2:17; then (f ") | (f .: [.p,g.]) is monotone by RELAT_1:72; then A5: (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is monotone by A1, A2, A3, Th19; (f ") .: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] = (f ") .: (f .: [.p,g.]) by A1, A2, A3, Th19 .= ((f ") | (f .: [.p,g.])) .: (f .: [.p,g.]) by RELAT_1:129 .= ((f | [.p,g.]) ") .: (f .: [.p,g.]) by RFUNCT_2:17 .= ((f | [.p,g.]) ") .: (rng (f | [.p,g.])) by RELAT_1:115 .= ((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) by FUNCT_1:33 .= rng ((f | [.p,g.]) ") by RELAT_1:113 .= dom (f | [.p,g.]) by FUNCT_1:33 .= (dom f) /\ [.p,g.] by RELAT_1:61 .= [.p,g.] by A2, XBOOLE_1:28 ; hence (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous by A1, A5, FCONT_1:46; ::_thesis: verum end; end; end; hence (f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is continuous ; ::_thesis: verum end;