:: NFCONT_2 semantic presentation begin definition let X be set ; let S, T be RealNormSpace; let f be PartFunc of S,T; predf is_uniformly_continuous_on X means :Def1: :: NFCONT_2:def 1 ( X c= dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r ) ) ) ); end; :: deftheorem Def1 defines is_uniformly_continuous_on NFCONT_2:def_1_:_ for X being set for S, T being RealNormSpace for f being PartFunc of S,T holds ( f is_uniformly_continuous_on X iff ( X c= dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r ) ) ) ) ); definition let X be set ; let S be RealNormSpace; let f be PartFunc of the carrier of S,REAL; predf is_uniformly_continuous_on X means :Def2: :: NFCONT_2:def 2 ( X c= dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds abs ((f /. x1) - (f /. x2)) < r ) ) ) ); end; :: deftheorem Def2 defines is_uniformly_continuous_on NFCONT_2:def_2_:_ for X being set for S being RealNormSpace for f being PartFunc of the carrier of S,REAL holds ( f is_uniformly_continuous_on X iff ( X c= dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds abs ((f /. x1) - (f /. x2)) < r ) ) ) ) ); theorem Th1: :: NFCONT_2:1 for X, X1 being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_uniformly_continuous_on X & X1 c= X holds f is_uniformly_continuous_on X1 proof let X, X1 be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st f is_uniformly_continuous_on X & X1 c= X holds f is_uniformly_continuous_on X1 let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_uniformly_continuous_on X & X1 c= X holds f is_uniformly_continuous_on X1 let f be PartFunc of S,T; ::_thesis: ( f is_uniformly_continuous_on X & X1 c= X implies f is_uniformly_continuous_on X1 ) assume that A1: f is_uniformly_continuous_on X and A2: X1 c= X ; ::_thesis: f is_uniformly_continuous_on X1 X c= dom f by A1, Def1; hence X1 c= dom f by A2, XBOOLE_1:1; :: according to NFCONT_2:def_1 ::_thesis: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r ) ) let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r ) ) then consider s being Real such that A3: 0 < s and A4: for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r by A1, Def1; take s ; ::_thesis: ( 0 < s & ( for x1, x2 being Point of S st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r ) ) thus 0 < s by A3; ::_thesis: for x1, x2 being Point of S st x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r let x1, x2 be Point of S; ::_thesis: ( x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s implies ||.((f /. x1) - (f /. x2)).|| < r ) assume ( x1 in X1 & x2 in X1 & ||.(x1 - x2).|| < s ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| < r hence ||.((f /. x1) - (f /. x2)).|| < r by A2, A4; ::_thesis: verum end; theorem :: NFCONT_2:2 for X, X1 being set for S, T being RealNormSpace for f1, f2 being PartFunc of S,T st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds f1 + f2 is_uniformly_continuous_on X /\ X1 proof let X, X1 be set ; ::_thesis: for S, T being RealNormSpace for f1, f2 being PartFunc of S,T st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds f1 + f2 is_uniformly_continuous_on X /\ X1 let S, T be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of S,T st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds f1 + f2 is_uniformly_continuous_on X /\ X1 let f1, f2 be PartFunc of S,T; ::_thesis: ( f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies f1 + f2 is_uniformly_continuous_on X /\ X1 ) assume that A1: f1 is_uniformly_continuous_on X and A2: f2 is_uniformly_continuous_on X1 ; ::_thesis: f1 + f2 is_uniformly_continuous_on X /\ X1 A3: f2 is_uniformly_continuous_on X /\ X1 by A2, Th1, XBOOLE_1:17; then A4: X /\ X1 c= dom f2 by Def1; A5: f1 is_uniformly_continuous_on X /\ X1 by A1, Th1, XBOOLE_1:17; then X /\ X1 c= dom f1 by Def1; then X /\ X1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:19; hence A6: X /\ X1 c= dom (f1 + f2) by VFUNCT_1:def_1; :: according to NFCONT_2:def_1 ::_thesis: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) ) let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) ) then A7: 0 < r / 2 by XREAL_1:215; then consider s being Real such that A8: 0 < s and A9: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds ||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A5, Def1; consider g being Real such that A10: 0 < g and A11: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < g holds ||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A3, A7, Def1; take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) ) thus 0 < p by A8, A10, XXREAL_0:15; ::_thesis: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r let x1, x2 be Point of S; ::_thesis: ( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p implies ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r ) assume that A12: x1 in X /\ X1 and A13: x2 in X /\ X1 and A14: ||.(x1 - x2).|| < p ; ::_thesis: ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r p <= g by XXREAL_0:17; then ||.(x1 - x2).|| < g by A14, XXREAL_0:2; then A15: ||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A11, A12, A13; p <= s by XXREAL_0:17; then ||.(x1 - x2).|| < s by A14, XXREAL_0:2; then ||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A9, A12, A13; then A16: ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) + (r / 2) by A15, XREAL_1:8; A17: ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by NORMSP_1:def_1; ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| = ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 + f2) /. x2)).|| by A6, A12, VFUNCT_1:def_1 .= ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 /. x2) + (f2 /. x2))).|| by A6, A13, VFUNCT_1:def_1 .= ||.((f1 /. x1) + ((f2 /. x1) - ((f1 /. x2) + (f2 /. x2)))).|| by RLVECT_1:def_3 .= ||.((f1 /. x1) + (((f2 /. x1) - (f1 /. x2)) - (f2 /. x2))).|| by RLVECT_1:27 .= ||.((f1 /. x1) + (((- (f1 /. x2)) + (f2 /. x1)) - (f2 /. x2))).|| .= ||.((f1 /. x1) + ((- (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def_3 .= ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:def_3 ; hence ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| < r by A16, A17, XXREAL_0:2; ::_thesis: verum end; theorem :: NFCONT_2:3 for X, X1 being set for S, T being RealNormSpace for f1, f2 being PartFunc of S,T st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds f1 - f2 is_uniformly_continuous_on X /\ X1 proof let X, X1 be set ; ::_thesis: for S, T being RealNormSpace for f1, f2 being PartFunc of S,T st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds f1 - f2 is_uniformly_continuous_on X /\ X1 let S, T be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of S,T st f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 holds f1 - f2 is_uniformly_continuous_on X /\ X1 let f1, f2 be PartFunc of S,T; ::_thesis: ( f1 is_uniformly_continuous_on X & f2 is_uniformly_continuous_on X1 implies f1 - f2 is_uniformly_continuous_on X /\ X1 ) assume that A1: f1 is_uniformly_continuous_on X and A2: f2 is_uniformly_continuous_on X1 ; ::_thesis: f1 - f2 is_uniformly_continuous_on X /\ X1 A3: f2 is_uniformly_continuous_on X /\ X1 by A2, Th1, XBOOLE_1:17; then A4: X /\ X1 c= dom f2 by Def1; A5: f1 is_uniformly_continuous_on X /\ X1 by A1, Th1, XBOOLE_1:17; then X /\ X1 c= dom f1 by Def1; then X /\ X1 c= (dom f1) /\ (dom f2) by A4, XBOOLE_1:19; hence A6: X /\ X1 c= dom (f1 - f2) by VFUNCT_1:def_2; :: according to NFCONT_2:def_1 ::_thesis: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) ) let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) ) then A7: 0 < r / 2 by XREAL_1:215; then consider s being Real such that A8: 0 < s and A9: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < s holds ||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A5, Def1; consider g being Real such that A10: 0 < g and A11: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < g holds ||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A3, A7, Def1; take p = min (s,g); ::_thesis: ( 0 < p & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) ) thus 0 < p by A8, A10, XXREAL_0:15; ::_thesis: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p holds ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r let x1, x2 be Point of S; ::_thesis: ( x1 in X /\ X1 & x2 in X /\ X1 & ||.(x1 - x2).|| < p implies ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r ) assume that A12: x1 in X /\ X1 and A13: x2 in X /\ X1 and A14: ||.(x1 - x2).|| < p ; ::_thesis: ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r p <= g by XXREAL_0:17; then ||.(x1 - x2).|| < g by A14, XXREAL_0:2; then A15: ||.((f2 /. x1) - (f2 /. x2)).|| < r / 2 by A11, A12, A13; p <= s by XXREAL_0:17; then ||.(x1 - x2).|| < s by A14, XXREAL_0:2; then ||.((f1 /. x1) - (f1 /. x2)).|| < r / 2 by A9, A12, A13; then A16: ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| < (r / 2) + (r / 2) by A15, XREAL_1:8; A17: ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by NORMSP_1:3; ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| = ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 - f2) /. x2)).|| by A6, A12, VFUNCT_1:def_2 .= ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).|| by A6, A13, VFUNCT_1:def_2 .= ||.((f1 /. x1) - ((f2 /. x1) + ((f1 /. x2) - (f2 /. x2)))).|| by RLVECT_1:27 .= ||.((f1 /. x1) - (((f1 /. x2) + (f2 /. x1)) - (f2 /. x2))).|| by RLVECT_1:def_3 .= ||.((f1 /. x1) - ((f1 /. x2) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def_3 .= ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:27 ; hence ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| < r by A16, A17, XXREAL_0:2; ::_thesis: verum end; theorem Th4: :: NFCONT_2:4 for X being set for p being Real for S, T being RealNormSpace for f being PartFunc of S,T st f is_uniformly_continuous_on X holds p (#) f is_uniformly_continuous_on X proof let X be set ; ::_thesis: for p being Real for S, T being RealNormSpace for f being PartFunc of S,T st f is_uniformly_continuous_on X holds p (#) f is_uniformly_continuous_on X let p be Real; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st f is_uniformly_continuous_on X holds p (#) f is_uniformly_continuous_on X let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_uniformly_continuous_on X holds p (#) f is_uniformly_continuous_on X let f be PartFunc of S,T; ::_thesis: ( f is_uniformly_continuous_on X implies p (#) f is_uniformly_continuous_on X ) assume A1: f is_uniformly_continuous_on X ; ::_thesis: p (#) f is_uniformly_continuous_on X then X c= dom f by Def1; hence A2: X c= dom (p (#) f) by VFUNCT_1:def_4; :: according to NFCONT_2:def_1 ::_thesis: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) ) now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_s_being_Real_st_ (_0_<_s_&_(_for_x1,_x2_being_Point_of_S_st_x1_in_X_&_x2_in_X_&_||.(x1_-_x2).||_<_s_holds_ ||.(((p_(#)_f)_/._x1)_-_((p_(#)_f)_/._x2)).||_<_r_)_) percases ( p = 0 or p <> 0 ) ; supposeA3: p = 0 ; ::_thesis: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.(((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 Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) ) ) assume A4: 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) ) then consider s being Real such that A5: 0 < s and for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r by A1, Def1; take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) ) thus 0 < s by A5; ::_thesis: for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r let x1, x2 be Point of S; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) assume that A6: x1 in X and A7: x2 in X and ||.(x1 - x2).|| < s ; ::_thesis: ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| = ||.((p * (f /. x1)) - ((p (#) f) /. x2)).|| by A2, A6, VFUNCT_1:def_4 .= ||.((0. T) - ((p (#) f) /. x2)).|| by A3, RLVECT_1:10 .= ||.((0. T) - (p * (f /. x2))).|| by A2, A7, VFUNCT_1:def_4 .= ||.((0. T) - (0. T)).|| by A3, RLVECT_1:10 .= ||.(0. T).|| by RLVECT_1:13 .= 0 by NORMSP_0:def_6 ; hence ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r by A4; ::_thesis: verum end; supposeA8: p <> 0 ; ::_thesis: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) ) then A9: 0 <> abs p by COMPLEX1:47; let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) ) ) A10: 0 < abs p by A8, COMPLEX1:47; assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) ) then 0 < r / (abs p) by A10, XREAL_1:139; then consider s being Real such that A11: 0 < s and A12: for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r / (abs p) by A1, Def1; take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) ) thus 0 < s by A11; ::_thesis: for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r let x1, x2 be Point of S; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) assume that A13: x1 in X and A14: x2 in X and A15: ||.(x1 - x2).|| < s ; ::_thesis: ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r A16: ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| = ||.((p * (f /. x1)) - ((p (#) f) /. x2)).|| by A2, A13, VFUNCT_1:def_4 .= ||.((p * (f /. x1)) - (p * (f /. x2))).|| by A2, A14, VFUNCT_1:def_4 .= ||.(p * ((f /. x1) - (f /. x2))).|| by RLVECT_1:34 .= (abs p) * ||.((f /. x1) - (f /. x2)).|| by NORMSP_1:def_1 ; (abs p) * ||.((f /. x1) - (f /. x2)).|| < (r / (abs p)) * (abs p) by A10, A12, A13, A14, A15, XREAL_1:68; hence ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r by A9, A16, XCMPLX_1:87; ::_thesis: verum end; end; end; hence for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| < r ) ) ; ::_thesis: verum end; theorem :: NFCONT_2:5 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_uniformly_continuous_on X holds - f is_uniformly_continuous_on X proof let X be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st f is_uniformly_continuous_on X holds - f is_uniformly_continuous_on X let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_uniformly_continuous_on X holds - f is_uniformly_continuous_on X let f be PartFunc of S,T; ::_thesis: ( f is_uniformly_continuous_on X implies - f is_uniformly_continuous_on X ) A1: - f = (- 1) (#) f by VFUNCT_1:23; assume f is_uniformly_continuous_on X ; ::_thesis: - f is_uniformly_continuous_on X hence - f is_uniformly_continuous_on X by A1, Th4; ::_thesis: verum end; theorem :: NFCONT_2:6 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_uniformly_continuous_on X holds ||.f.|| is_uniformly_continuous_on X proof let X be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st f is_uniformly_continuous_on X holds ||.f.|| is_uniformly_continuous_on X let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_uniformly_continuous_on X holds ||.f.|| is_uniformly_continuous_on X let f be PartFunc of S,T; ::_thesis: ( f is_uniformly_continuous_on X implies ||.f.|| is_uniformly_continuous_on X ) assume A1: f is_uniformly_continuous_on X ; ::_thesis: ||.f.|| is_uniformly_continuous_on X then X c= dom f by Def1; hence A2: X c= dom ||.f.|| by NORMSP_0:def_3; :: according to NFCONT_2:def_2 ::_thesis: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(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 Point of S st x1 in X & x2 in X & ||.(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 Point of S st x1 in X & x2 in X & ||.(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 Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r by A1, Def1; take s ; ::_thesis: ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) ) thus 0 < s by A3; ::_thesis: for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r let x1, x2 be Point of S; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r ) assume that A5: x1 in X and A6: x2 in X and A7: ||.(x1 - x2).|| < s ; ::_thesis: abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r abs ((||.f.|| /. x1) - (||.f.|| /. x2)) = abs ((||.f.|| . x1) - (||.f.|| /. x2)) by A2, A5, PARTFUN1:def_6 .= abs ((||.f.|| . x1) - (||.f.|| . x2)) by A2, A6, PARTFUN1:def_6 .= abs (||.(f /. x1).|| - (||.f.|| . x2)) by A2, A5, NORMSP_0:def_3 .= abs (||.(f /. x1).|| - ||.(f /. x2).||) by A2, A6, NORMSP_0:def_3 ; then A8: abs ((||.f.|| /. x1) - (||.f.|| /. x2)) <= ||.((f /. x1) - (f /. x2)).|| by NORMSP_1:9; ||.((f /. x1) - (f /. x2)).|| < r by A4, A5, A6, A7; hence abs ((||.f.|| /. x1) - (||.f.|| /. x2)) < r by A8, XXREAL_0:2; ::_thesis: verum end; theorem Th7: :: NFCONT_2:7 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_uniformly_continuous_on X holds f is_continuous_on X proof let X be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st f is_uniformly_continuous_on X holds f is_continuous_on X let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_uniformly_continuous_on X holds f is_continuous_on X let f be PartFunc of S,T; ::_thesis: ( f is_uniformly_continuous_on X implies f is_continuous_on X ) assume A1: f is_uniformly_continuous_on X ; ::_thesis: f is_continuous_on X A2: now__::_thesis:_for_x0_being_Point_of_S for_r_being_Real_st_x0_in_X_&_0_<_r_holds_ ex_s_being_Real_st_ (_0_<_s_&_(_for_x1_being_Point_of_S_st_x1_in_X_&_||.(x1_-_x0).||_<_s_holds_ ||.((f_/._x1)_-_(f_/._x0)).||_<_r_)_) let x0 be Point of S; ::_thesis: for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) assume that A3: x0 in X and A4: 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) consider s being Real such that A5: 0 < s and A6: for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r by A1, A4, Def1; take s = s; ::_thesis: ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) thus 0 < s by A5; ::_thesis: for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r let x1 be Point of S; ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies ||.((f /. x1) - (f /. x0)).|| < r ) assume ( x1 in X & ||.(x1 - x0).|| < s ) ; ::_thesis: ||.((f /. x1) - (f /. x0)).|| < r hence ||.((f /. x1) - (f /. x0)).|| < r by A3, A6; ::_thesis: verum end; X c= dom f by A1, Def1; hence f is_continuous_on X by A2, NFCONT_1:19; ::_thesis: verum end; theorem Th8: :: NFCONT_2:8 for X being set for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st f is_uniformly_continuous_on X holds f is_continuous_on X proof let X be set ; ::_thesis: for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st f is_uniformly_continuous_on X holds f is_continuous_on X let S be RealNormSpace; ::_thesis: for f being PartFunc of the carrier of S,REAL st f is_uniformly_continuous_on X holds f is_continuous_on X let f be PartFunc of the carrier of S,REAL; ::_thesis: ( f is_uniformly_continuous_on X implies f is_continuous_on X ) assume A1: f is_uniformly_continuous_on X ; ::_thesis: f is_continuous_on X A2: now__::_thesis:_for_x0_being_Point_of_S for_r_being_Real_st_x0_in_X_&_0_<_r_holds_ ex_s_being_Real_st_ (_0_<_s_&_(_for_x1_being_Point_of_S_st_x1_in_X_&_||.(x1_-_x0).||_<_s_holds_ abs_((f_/._x1)_-_(f_/._x0))_<_r_)_) let x0 be Point of S; ::_thesis: for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(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 st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) consider s being Real such that A5: 0 < s and A6: for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds abs ((f /. x1) - (f /. x2)) < r by A1, A4, Def2; take s = s; ::_thesis: ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) thus 0 < s by A5; ::_thesis: for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r let x1 be Point of S; ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies abs ((f /. x1) - (f /. x0)) < r ) assume ( x1 in X & ||.(x1 - x0).|| < s ) ; ::_thesis: abs ((f /. x1) - (f /. x0)) < r hence abs ((f /. x1) - (f /. x0)) < r by A3, A6; ::_thesis: verum end; X c= dom f by A1, Def2; hence f is_continuous_on X by A2, NFCONT_1:20; ::_thesis: verum end; theorem Th9: :: NFCONT_2:9 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X holds f is_uniformly_continuous_on X proof let X be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X holds f is_uniformly_continuous_on X let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_Lipschitzian_on X holds f is_uniformly_continuous_on X let f be PartFunc of S,T; ::_thesis: ( f is_Lipschitzian_on X implies f is_uniformly_continuous_on X ) assume A1: f is_Lipschitzian_on X ; ::_thesis: f is_uniformly_continuous_on X hence X c= dom f by NFCONT_1:def_9; :: according to NFCONT_2:def_1 ::_thesis: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r ) ) consider r being Real such that A2: 0 < r and A3: for x1, x2 being Point of S st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| by A1, NFCONT_1:def_9; let p be Real; ::_thesis: ( 0 < p implies ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < p ) ) ) assume A4: 0 < p ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < p ) ) take s = p / r; ::_thesis: ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < p ) ) thus 0 < s by A2, A4, XREAL_1:139; ::_thesis: for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < p let x1, x2 be Point of S; ::_thesis: ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.((f /. x1) - (f /. x2)).|| < p ) assume ( x1 in X & x2 in X & ||.(x1 - x2).|| < s ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| < p then ( r * ||.(x1 - x2).|| < s * r & ||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) by A2, A3, XREAL_1:68; then ||.((f /. x1) - (f /. x2)).|| < (p / r) * r by XXREAL_0:2; hence ||.((f /. x1) - (f /. x2)).|| < p by A2, XCMPLX_1:87; ::_thesis: verum end; theorem :: NFCONT_2:10 for T, S being RealNormSpace for f being PartFunc of S,T for Y being Subset of S st Y is compact & f is_continuous_on Y holds f is_uniformly_continuous_on Y proof let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T for Y being Subset of S st Y is compact & f is_continuous_on Y holds f is_uniformly_continuous_on Y let f be PartFunc of S,T; ::_thesis: for Y being Subset of S st Y is compact & f is_continuous_on Y holds f is_uniformly_continuous_on Y let Y be Subset of S; ::_thesis: ( Y is compact & f is_continuous_on Y implies f is_uniformly_continuous_on Y ) assume that A1: Y is compact and A2: f is_continuous_on Y ; ::_thesis: f is_uniformly_continuous_on Y A3: Y c= dom f by A2, NFCONT_1:def_7; assume not f is_uniformly_continuous_on Y ; ::_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 Point of S st ( x1 in Y & x2 in Y & ||.(x1 - x2).|| < s & not ||.((f /. x1) - (f /. x2)).|| < r ) by A3, Def1; defpred S1[ Element of NAT , Point of S] means ( \$2 in Y & ex x2 being Point of S st ( x2 in Y & ||.(\$2 - x2).|| < 1 / (\$1 + 1) & not ||.((f /. \$2) - (f /. x2)).|| < r ) ); A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<_1_/_(n_+_1) let n be Element of NAT ; ::_thesis: 0 < 1 / (n + 1) 0 < n + 1 by NAT_1:5; hence 0 < 1 / (n + 1) by XREAL_1:139; ::_thesis: verum end; A7: now__::_thesis:_for_n_being_Element_of_NAT_ex_x1_being_Point_of_S_st_S1[n,x1] let n be Element of NAT ; ::_thesis: ex x1 being Point of S st S1[n,x1] consider x1 being Point of S such that A8: ex x2 being Point of S st ( x1 in Y & x2 in Y & ||.(x1 - x2).|| < 1 / (n + 1) & not ||.((f /. x1) - (f /. x2)).|| < r ) by A5, A6; take x1 = x1; ::_thesis: S1[n,x1] thus S1[n,x1] by A8; ::_thesis: verum end; consider s1 being sequence of S such that A9: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A7); defpred S2[ Element of NAT , Point of S] means ( \$2 in Y & ||.((s1 . \$1) - \$2).|| < 1 / (\$1 + 1) & not ||.((f /. (s1 . \$1)) - (f /. \$2)).|| < r ); A10: for n being Element of NAT ex x2 being Point of S st S2[n,x2] by A9; consider s2 being sequence of S such that A11: for n being Element of NAT holds S2[n,s2 . n] from FUNCT_2:sch_3(A10); 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 NFCONT_1:6; hence x in Y by A9; ::_thesis: verum end; then A12: rng s1 c= Y by TARSKI:def_3; then consider q1 being sequence of S such that A13: q1 is subsequence of s1 and A14: q1 is convergent and A15: lim q1 in Y by A1, NFCONT_1:def_2; consider Ns1 being increasing sequence of NAT such that A16: q1 = s1 * Ns1 by A13, VALUED_0:def_17; set q2 = q1 - ((s1 - s2) * Ns1); A17: f | Y is_continuous_in lim q1 by A2, A15, NFCONT_1:def_7; 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 NFCONT_1:6; hence x in Y by A11; ::_thesis: verum end; then A18: rng s2 c= Y by TARSKI:def_3; 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 A16, NORMSP_1:def_3 .= (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 NORMSP_1:def_3 .= ((s1 . (Ns1 . n)) - (s1 . (Ns1 . n))) + (s2 . (Ns1 . n)) by RLVECT_1:29 .= (0. S) + (s2 . (Ns1 . n)) by RLVECT_1:15 .= s2 . (Ns1 . n) by RLVECT_1:4 .= (s2 * Ns1) . n by FUNCT_2:15 ; ::_thesis: verum end; then A19: q1 - ((s1 - s2) * Ns1) = s2 * Ns1 by FUNCT_2:63; then rng (q1 - ((s1 - s2) * Ns1)) c= rng s2 by VALUED_0:21; then A20: rng (q1 - ((s1 - s2) * Ns1)) c= Y by A18, XBOOLE_1:1; then rng (q1 - ((s1 - s2) * Ns1)) c= dom f by A3, XBOOLE_1:1; then rng (q1 - ((s1 - s2) * Ns1)) c= (dom f) /\ Y by A20, XBOOLE_1:19; then A21: rng (q1 - ((s1 - s2) * Ns1)) c= dom (f | Y) by RELAT_1:61; A22: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ ||.(((s1_-_s2)_._m)_-_(0._S)).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st for m being Element of NAT st k <= m holds ||.(((s1 - s2) . m) - (0. S)).|| < p ) assume A23: 0 < p ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds ||.(((s1 - s2) . m) - (0. S)).|| < p A24: 0 < p " by A23; consider k being Element of NAT such that A25: p " < k by SEQ_4:3; take k = k; ::_thesis: for m being Element of NAT st k <= m holds ||.(((s1 - s2) . m) - (0. S)).|| < p let m be Element of NAT ; ::_thesis: ( k <= m implies ||.(((s1 - s2) . m) - (0. S)).|| < p ) assume k <= m ; ::_thesis: ||.(((s1 - s2) . m) - (0. S)).|| < p then k + 1 <= m + 1 by XREAL_1:6; then 1 / (m + 1) <= 1 / (k + 1) by A25, A24, XREAL_1:118; then A26: ||.((s1 . m) - (s2 . m)).|| < 1 / (k + 1) by A11, XXREAL_0:2; k < k + 1 by NAT_1:13; then p " < k + 1 by A25, XXREAL_0:2; then 1 / (k + 1) < 1 / (p ") by A23, XREAL_1:76; then A27: 1 / (k + 1) < p by XCMPLX_1:216; ||.(((s1 - s2) . m) - (0. S)).|| = ||.(((s1 . m) - (s2 . m)) - (0. S)).|| by NORMSP_1:def_3 .= ||.((s1 . m) - (s2 . m)).|| by RLVECT_1:13 ; hence ||.(((s1 - s2) . m) - (0. S)).|| < p by A27, A26, XXREAL_0:2; ::_thesis: verum end; then A28: s1 - s2 is convergent by NORMSP_1:def_6; then A29: (s1 - s2) * Ns1 is convergent by LOPBAN_3:7; then A30: q1 - ((s1 - s2) * Ns1) is convergent by A14, NORMSP_1:20; rng q1 c= rng s1 by A13, VALUED_0:21; then A31: rng q1 c= Y by A12, XBOOLE_1:1; then rng q1 c= dom f by A3, XBOOLE_1:1; then rng q1 c= (dom f) /\ Y by A31, XBOOLE_1:19; then A32: rng q1 c= dom (f | Y) by RELAT_1:61; then A33: (f | Y) /. (lim q1) = lim ((f | Y) /* q1) by A14, A17, NFCONT_1:def_5; A34: (f | Y) /* q1 is convergent by A14, A17, A32, NFCONT_1:def_5; lim (s1 - s2) = 0. S by A22, A28, NORMSP_1:def_7; then lim ((s1 - s2) * Ns1) = 0. S by A28, LOPBAN_3:8; then A35: lim (q1 - ((s1 - s2) * Ns1)) = (lim q1) - (0. S) by A14, A29, NORMSP_1:26 .= lim q1 by RLVECT_1:13 ; then A36: (f | Y) /* (q1 - ((s1 - s2) * Ns1)) is convergent by A17, A30, A21, NFCONT_1:def_5; then A37: ((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) is convergent by A34, NORMSP_1:20; (f | Y) /. (lim q1) = lim ((f | Y) /* (q1 - ((s1 - s2) * Ns1))) by A17, A30, A35, A21, NFCONT_1:def_5; then A38: lim (((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) = ((f | Y) /. (lim q1)) - ((f | Y) /. (lim q1)) by A34, A33, A36, NORMSP_1:26 .= 0. T by RLVECT_1:15 ; 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 ||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . m) - (0. T)).|| < r by A4, A37, A38, NORMSP_1:def_7; A40: q1 . k in rng q1 by NFCONT_1:6; A41: (q1 - ((s1 - s2) * Ns1)) . k in rng (q1 - ((s1 - s2) * Ns1)) by NFCONT_1:6; ||.(((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k) - (0. T)).|| = ||.((((f | Y) /* q1) - ((f | Y) /* (q1 - ((s1 - s2) * Ns1)))) . k).|| by RLVECT_1:13 .= ||.((((f | Y) /* q1) . k) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by NORMSP_1:def_3 .= ||.(((f | Y) /. (q1 . k)) - (((f | Y) /* (q1 - ((s1 - s2) * Ns1))) . k)).|| by A32, FUNCT_2:109 .= ||.(((f | Y) /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A21, FUNCT_2:109 .= ||.((f /. (q1 . k)) - ((f | Y) /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A32, A40, PARTFUN2:15 .= ||.((f /. (q1 . k)) - (f /. ((q1 - ((s1 - s2) * Ns1)) . k))).|| by A21, A41, PARTFUN2:15 .= ||.((f /. (s1 . (Ns1 . k))) - (f /. ((s2 * Ns1) . k))).|| by A16, A19, FUNCT_2:15 .= ||.((f /. (s1 . (Ns1 . k))) - (f /. (s2 . (Ns1 . k)))).|| by FUNCT_2:15 ; hence contradiction by A11, A39; ::_thesis: verum end; hence contradiction ; ::_thesis: verum end; theorem :: NFCONT_2:11 for T, S being RealNormSpace for f being PartFunc of S,T for Y being Subset of S st Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds f .: Y is compact by Th7, NFCONT_1:32; theorem :: NFCONT_2:12 for S being RealNormSpace for f being PartFunc of the carrier of S,REAL for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_uniformly_continuous_on Y holds ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) by Th8, NFCONT_1:37; theorem :: NFCONT_2:13 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st X c= dom f & f | X is constant holds f is_uniformly_continuous_on X by Th9, NFCONT_1:43; begin definition let M be non empty NORMSTR ; let f be Function of M,M; attrf is contraction means :Def3: :: NFCONT_2:def 3 ex L being Real st ( 0 < L & L < 1 & ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= L * ||.(x - y).|| ) ); end; :: deftheorem Def3 defines contraction NFCONT_2:def_3_:_ for M being non empty NORMSTR for f being Function of M,M holds ( f is contraction iff ex L being Real st ( 0 < L & L < 1 & ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= L * ||.(x - y).|| ) ) ); registration let M be RealNormSpace; cluster non empty Relation-like the carrier of M -defined the carrier of M -valued Function-like total quasi_total contraction for Element of K6(K7( the carrier of M, the carrier of M)); existence ex b1 being Function of M,M st b1 is contraction proof set x = the Point of M; reconsider f = the carrier of M --> the Point of M as Function of the carrier of M, the carrier of M ; take f ; ::_thesis: f is contraction take 1 / 2 ; :: according to NFCONT_2:def_3 ::_thesis: ( 0 < 1 / 2 & 1 / 2 < 1 & ( for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= (1 / 2) * ||.(x - y).|| ) ) thus ( 0 < 1 / 2 & 1 / 2 < 1 ) ; ::_thesis: for x, y being Point of M holds ||.((f . x) - (f . y)).|| <= (1 / 2) * ||.(x - y).|| let z, y be Point of M; ::_thesis: ||.((f . z) - (f . y)).|| <= (1 / 2) * ||.(z - y).|| ( f . z = the Point of M & f . y = the Point of M ) by FUNCOP_1:7; then ||.((f . z) - (f . y)).|| = 0 by NORMSP_1:6; hence ||.((f . z) - (f . y)).|| <= (1 / 2) * ||.(z - y).|| ; ::_thesis: verum end; end; definition let M be RealNormSpace; mode Contraction of M is contraction Function of M,M; end; Lm1: ( ( for X being RealNormSpace for x, y being Point of X holds ( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace for x, y being Point of X holds ( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace for x, y being Point of X holds ( ||.(x - y).|| > 0 iff x <> y ) ) & ( for X being RealNormSpace for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| ) & ( for X being RealNormSpace for x, y, z being Point of X for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds ||.(x - y).|| < e ) & ( for X being RealNormSpace for x, y, z being Point of X for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds ||.(x - y).|| < e ) & ( for X being RealNormSpace for x being Point of X st ( for e being Real st e > 0 holds ||.x.|| < e ) holds x = 0. X ) & ( for X being RealNormSpace for x, y being Point of X st ( for e being Real st e > 0 holds ||.(x - y).|| < e ) holds x = y ) ) proof A1: for X being RealNormSpace for x, y, z being Point of X for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds ||.(x - y).|| < e proof let X be RealNormSpace; ::_thesis: for x, y, z being Point of X for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds ||.(x - y).|| < e let x, y, z be Point of X; ::_thesis: for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds ||.(x - y).|| < e let e be Real; ::_thesis: ( e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 implies ||.(x - y).|| < e ) assume e > 0 ; ::_thesis: ( not ||.(x - z).|| < e / 2 or not ||.(z - y).|| < e / 2 or ||.(x - y).|| < e ) assume ( ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 ) ; ::_thesis: ||.(x - y).|| < e then ||.(x - z).|| + ||.(z - y).|| < (e / 2) + (e / 2) by XREAL_1:8; then ||.(x - y).|| + (||.(x - z).|| + ||.(z - y).||) < (||.(x - z).|| + ||.(z - y).||) + e by NORMSP_1:10, XREAL_1:8; then (||.(x - y).|| + (||.(x - z).|| + ||.(z - y).||)) + (- (||.(x - z).|| + ||.(z - y).||)) < (e + (||.(x - z).|| + ||.(z - y).||)) + (- (||.(x - z).|| + ||.(z - y).||)) by XREAL_1:8; hence ||.(x - y).|| < e ; ::_thesis: verum end; A2: for X being RealNormSpace for x, y, z being Point of X for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds ||.(x - y).|| < e proof let X be RealNormSpace; ::_thesis: for x, y, z being Point of X for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds ||.(x - y).|| < e let x, y, z be Point of X; ::_thesis: for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds ||.(x - y).|| < e let e be Real; ::_thesis: ( e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 implies ||.(x - y).|| < e ) assume A3: e > 0 ; ::_thesis: ( not ||.(x - z).|| < e / 2 or not ||.(y - z).|| < e / 2 or ||.(x - y).|| < e ) assume that A4: ||.(x - z).|| < e / 2 and A5: ||.(y - z).|| < e / 2 ; ::_thesis: ||.(x - y).|| < e ||.(- (y - z)).|| < e / 2 by A5, NORMSP_1:2; then ||.(z - y).|| < e / 2 by RLVECT_1:33; hence ||.(x - y).|| < e by A1, A3, A4; ::_thesis: verum end; A6: for X being RealNormSpace for x, y being Point of X holds ( ||.(x - y).|| > 0 iff x <> y ) proof let X be RealNormSpace; ::_thesis: for x, y being Point of X holds ( ||.(x - y).|| > 0 iff x <> y ) let x, y be Point of X; ::_thesis: ( ||.(x - y).|| > 0 iff x <> y ) ( 0 < ||.(x - y).|| implies x - y <> 0. X ) by NORMSP_0:def_6; hence ( 0 < ||.(x - y).|| implies x <> y ) by RLVECT_1:15; ::_thesis: ( x <> y implies ||.(x - y).|| > 0 ) now__::_thesis:_(_x_<>_y_implies_0_<_||.(x_-_y).||_) assume x <> y ; ::_thesis: 0 < ||.(x - y).|| then 0 <> ||.(x - y).|| by NORMSP_1:11; hence 0 < ||.(x - y).|| ; ::_thesis: verum end; hence ( x <> y implies ||.(x - y).|| > 0 ) ; ::_thesis: verum end; A7: for X being RealNormSpace for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| proof let X be RealNormSpace; ::_thesis: for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| let x, y be Point of X; ::_thesis: ||.(x - y).|| = ||.(y - x).|| thus ||.(x - y).|| = ||.(- (x - y)).|| by NORMSP_1:2 .= ||.(y - x).|| by RLVECT_1:33 ; ::_thesis: verum end; A8: for X being RealNormSpace for x being Point of X st ( for e being Real st e > 0 holds ||.x.|| < e ) holds x = 0. X proof let X be RealNormSpace; ::_thesis: for x being Point of X st ( for e being Real st e > 0 holds ||.x.|| < e ) holds x = 0. X let x be Point of X; ::_thesis: ( ( for e being Real st e > 0 holds ||.x.|| < e ) implies x = 0. X ) assume A9: for e being Real st e > 0 holds ||.x.|| < e ; ::_thesis: x = 0. X now__::_thesis:_not_x_<>_0._X assume x <> 0. X ; ::_thesis: contradiction then 0 <> ||.x.|| by NORMSP_0:def_5; then 0 < ||.x.|| ; hence contradiction by A9; ::_thesis: verum end; hence x = 0. X ; ::_thesis: verum end; thus ( ( for X being RealNormSpace for x, y being Point of X holds ( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace for x, y being Point of X holds ( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace for x, y being Point of X holds ( ||.(x - y).|| > 0 iff x <> y ) ) & ( for X being RealNormSpace for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| ) & ( for X being RealNormSpace for x, y, z being Point of X for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds ||.(x - y).|| < e ) & ( for X being RealNormSpace for x, y, z being Point of X for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds ||.(x - y).|| < e ) & ( for X being RealNormSpace for x being Point of X st ( for e being Real st e > 0 holds ||.x.|| < e ) holds x = 0. X ) & ( for X being RealNormSpace for x, y being Point of X st ( for e being Real st e > 0 holds ||.(x - y).|| < e ) holds x = y ) ) by A6, A7, A1, A2, A8; ::_thesis: verum end; Lm2: for K, L, e being real number st 0 < K & K < 1 & 0 < e holds ex n being Element of NAT st abs (L * (K to_power n)) < e proof let K, L, e be real number ; ::_thesis: ( 0 < K & K < 1 & 0 < e implies ex n being Element of NAT st abs (L * (K to_power n)) < e ) assume that A1: ( 0 < K & K < 1 ) and A2: 0 < e ; ::_thesis: ex n being Element of NAT st abs (L * (K to_power n)) < e deffunc H1( Element of NAT ) -> set = K to_power (\$1 + 1); consider rseq being Real_Sequence such that A3: for n being Element of NAT holds rseq . n = H1(n) from SEQ_1:sch_1(); A4: L (#) rseq is convergent by A1, A3, SEQ_2:7, SERIES_1:1; A5: lim rseq = 0 by A1, A3, SERIES_1:1; lim (L (#) rseq) = L * (lim rseq) by A1, A3, SEQ_2:8, SERIES_1:1 .= 0 by A5 ; then consider n being Element of NAT such that A6: for m being Element of NAT st n <= m holds abs (((L (#) rseq) . m) - 0) < e by A2, A4, SEQ_2:def_7; abs (((L (#) rseq) . n) - 0) < e by A6; then abs (L * (rseq . n)) < e by SEQ_1:9; then abs (L * (K to_power (n + 1))) < e by A3; hence ex n being Element of NAT st abs (L * (K to_power n)) < e ; ::_thesis: verum end; theorem Th14: :: NFCONT_2:14 for X being RealBanachSpace for f being Function of X,X st f is Contraction of X holds ex xp being Point of X st ( f . xp = xp & ( for x being Point of X st f . x = x holds xp = x ) ) proof let X be RealBanachSpace; ::_thesis: for f being Function of X,X st f is Contraction of X holds ex xp being Point of X st ( f . xp = xp & ( for x being Point of X st f . x = x holds xp = x ) ) set x0 = the Element of X; let f be Function of X,X; ::_thesis: ( f is Contraction of X implies ex xp being Point of X st ( f . xp = xp & ( for x being Point of X st f . x = x holds xp = x ) ) ) assume f is Contraction of X ; ::_thesis: ex xp being Point of X st ( f . xp = xp & ( for x being Point of X st f . x = x holds xp = x ) ) then consider K being Real such that A1: 0 < K and A2: K < 1 and A3: for x, y being Point of X holds ||.((f . x) - (f . y)).|| <= K * ||.(x - y).|| by Def3; deffunc H1( set , set ) -> set = f . \$2; consider g being Function such that A4: ( dom g = NAT & g . 0 = the Element of X & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) ) from NAT_1:sch_11(); defpred S1[ Element of NAT ] means g . \$1 in the carrier of X; A5: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: S1[k] ; ::_thesis: S1[k + 1] g . (k + 1) = f . (g . k) by A4; hence S1[k + 1] by A6, FUNCT_2:5; ::_thesis: verum end; A7: S1[ 0 ] by A4; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A5); then for n being set st n in NAT holds g . n in the carrier of X ; then reconsider g = g as sequence of X by A4, FUNCT_2:3; A8: now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(((g_^\_1)_._n)_-_(f_._(lim_g))).||_<=_K_*_||.((g_._n)_-_(lim_g)).|| let n be Element of NAT ; ::_thesis: ||.(((g ^\ 1) . n) - (f . (lim g))).|| <= K * ||.((g . n) - (lim g)).|| ||.(((g ^\ 1) . n) - (f . (lim g))).|| = ||.((g . (n + 1)) - (f . (lim g))).|| by NAT_1:def_3 .= ||.((f . (g . n)) - (f . (lim g))).|| by A4 ; hence ||.(((g ^\ 1) . n) - (f . (lim g))).|| <= K * ||.((g . n) - (lim g)).|| by A3; ::_thesis: verum end; A9: for n being Element of NAT holds ||.((g . (n + 1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power n) proof defpred S2[ Element of NAT ] means ||.((g . (\$1 + 1)) - (g . \$1)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power \$1); A10: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume S2[k] ; ::_thesis: S2[k + 1] then A11: K * ||.((g . (k + 1)) - (g . k)).|| <= K * (||.((g . 1) - (g . 0)).|| * (K to_power k)) by A1, XREAL_1:64; ||.((f . (g . (k + 1))) - (f . (g . k))).|| <= K * ||.((g . (k + 1)) - (g . k)).|| by A3; then ||.((f . (g . (k + 1))) - (f . (g . k))).|| <= ||.((g . 1) - (g . 0)).|| * (K * (K to_power k)) by A11, XXREAL_0:2; then A12: ||.((f . (g . (k + 1))) - (f . (g . k))).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power 1) * (K to_power k)) by POWER:25; g . (k + 1) = f . (g . k) by A4; then ||.((g . ((k + 1) + 1)) - (g . (k + 1))).|| = ||.((f . (g . (k + 1))) - (f . (g . k))).|| by A4; hence S2[k + 1] by A1, A12, POWER:27; ::_thesis: verum end; ||.((g . (0 + 1)) - (g . 0)).|| = ||.((g . 1) - (g . 0)).|| * 1 .= ||.((g . 1) - (g . 0)).|| * (K to_power 0) by POWER:24 ; then A13: S2[ 0 ] ; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A13, A10); hence for n being Element of NAT holds ||.((g . (n + 1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power n) ; ::_thesis: verum end; A14: for k, n being Element of NAT holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)) proof defpred S2[ Element of NAT ] means for n being Element of NAT holds ||.((g . (n + \$1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + \$1))) / (1 - K)); A15: now__::_thesis:_for_k_being_Element_of_NAT_st_S2[k]_holds_ S2[k_+_1] let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A16: S2[k] ; ::_thesis: S2[k + 1] now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((g_._(n_+_(k_+_1)))_-_(g_._n)).||_<=_||.((g_._1)_-_(g_._0)).||_*_(((K_to_power_n)_-_(K_to_power_(n_+_(k_+_1))))_/_(1_-_K)) let n be Element of NAT ; ::_thesis: ||.((g . (n + (k + 1))) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + (k + 1)))) / (1 - K)) 1 - K <> 0 by A2; then A17: (||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + (||.((g . 1) - (g . 0)).|| * (K to_power (n + k))) = (||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + (((||.((g . 1) - (g . 0)).|| * (K to_power (n + k))) * (1 - K)) / (1 - K)) by XCMPLX_1:89 .= (||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + ((||.((g . 1) - (g . 0)).|| * ((K to_power (n + k)) * (1 - K))) / (1 - K)) .= (||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) + (||.((g . 1) - (g . 0)).|| * (((K to_power (n + k)) * (1 - K)) / (1 - K))) by XCMPLX_1:74 .= ||.((g . 1) - (g . 0)).|| * ((((K to_power n) - (K to_power (n + k))) / (1 - K)) + (((K to_power (n + k)) * (1 - K)) / (1 - K))) .= ||.((g . 1) - (g . 0)).|| * ((((K to_power n) - (K to_power (n + k))) + ((K to_power (n + k)) * (1 - K))) / (1 - K)) by XCMPLX_1:62 .= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K * (K to_power (n + k)))) / (1 - K)) .= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - ((K to_power 1) * (K to_power (n + k)))) / (1 - K)) by POWER:25 .= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power ((n + k) + 1))) / (1 - K)) by A1, POWER:27 ; ( ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)) & ||.((g . ((n + k) + 1)) - (g . (n + k))).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power (n + k)) ) by A9, A16; then ( ||.((g . (n + (k + 1))) - (g . n)).|| <= ||.((g . (n + (k + 1))) - (g . (n + k))).|| + ||.((g . (n + k)) - (g . n)).|| & ||.((g . (n + (k + 1))) - (g . (n + k))).|| + ||.((g . (n + k)) - (g . n)).|| <= (||.((g . 1) - (g . 0)).|| * (K to_power (n + k))) + (||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K))) ) by NORMSP_1:10, XREAL_1:7; hence ||.((g . (n + (k + 1))) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + (k + 1)))) / (1 - K)) by A17, XXREAL_0:2; ::_thesis: verum end; hence S2[k + 1] ; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((g_._(n_+_0))_-_(g_._n)).||_<=_||.((g_._1)_-_(g_._0)).||_*_(((K_to_power_n)_-_(K_to_power_(n_+_0)))_/_(1_-_K)) let n be Element of NAT ; ::_thesis: ||.((g . (n + 0)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + 0))) / (1 - K)) ||.((g . (n + 0)) - (g . n)).|| = ||.(0. X).|| by RLVECT_1:15 .= 0 by NORMSP_1:1 ; hence ||.((g . (n + 0)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + 0))) / (1 - K)) ; ::_thesis: verum end; then A18: S2[ 0 ] ; for k being Element of NAT holds S2[k] from NAT_1:sch_1(A18, A15); hence for k, n being Element of NAT holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)) ; ::_thesis: verum end; A19: for k, n being Element of NAT holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) proof let k be Element of NAT ; ::_thesis: for n being Element of NAT holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((g_._(n_+_k))_-_(g_._n)).||_<=_||.((g_._1)_-_(g_._0)).||_*_((K_to_power_n)_/_(1_-_K)) let n be Element of NAT ; ::_thesis: ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) K to_power (n + k) > 0 by A1, POWER:34; then A21: (K to_power n) - (K to_power (n + k)) <= (K to_power n) - 0 by XREAL_1:13; 1 - K > 1 - 1 by A2, XREAL_1:15; then ((K to_power n) - (K to_power (n + k))) / (1 - K) <= (K to_power n) / (1 - K) by A21, XREAL_1:72; then A22: ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)) <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) by XREAL_1:64; ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + k))) / (1 - K)) by A14; hence ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) by A22, XXREAL_0:2; ::_thesis: verum end; hence for n being Element of NAT holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) ; ::_thesis: verum end; now__::_thesis:_for_e_being_Real_st_e_>_0_holds_ ex_nn_being_Element_of_NAT_st_ for_n,_m_being_Element_of_NAT_st_n_>=_nn_&_m_>=_nn_holds_ ||.((g_._n)_-_(g_._m)).||_<_e let e be Real; ::_thesis: ( e > 0 implies ex nn being Element of NAT st for n, m being Element of NAT st n >= nn & m >= nn holds ||.((g . n) - (g . m)).|| < e ) assume A23: e > 0 ; ::_thesis: ex nn being Element of NAT st for n, m being Element of NAT st n >= nn & m >= nn holds ||.((g . n) - (g . m)).|| < e e / 2 > 0 by A23, XREAL_1:215; then consider n being Element of NAT such that A24: abs ((||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n)) < e / 2 by A1, A2, Lm2; take nn = n + 1; ::_thesis: for n, m being Element of NAT st n >= nn & m >= nn holds ||.((g . n) - (g . m)).|| < e (||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n) <= abs ((||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n)) by ABSVALUE:4; then (||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n) < e / 2 by A24, XXREAL_0:2; then A25: ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) < e / 2 by XCMPLX_1:75; now__::_thesis:_for_m,_l_being_Element_of_NAT_st_nn_<=_m_&_nn_<=_l_holds_ ||.((g_._l)_-_(g_._m)).||_<_e let m, l be Element of NAT ; ::_thesis: ( nn <= m & nn <= l implies ||.((g . l) - (g . m)).|| < e ) assume that A26: nn <= m and A27: nn <= l ; ::_thesis: ||.((g . l) - (g . m)).|| < e n < m by A26, NAT_1:13; then consider k1 being Nat such that A28: n + k1 = m by NAT_1:10; n < l by A27, NAT_1:13; then consider k2 being Nat such that A29: n + k2 = l by NAT_1:10; reconsider k2 = k2 as Element of NAT by ORDINAL1:def_12; ||.((g . (n + k2)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) by A19; then A30: ||.((g . l) - (g . n)).|| < e / 2 by A25, A29, XXREAL_0:2; reconsider k1 = k1 as Element of NAT by ORDINAL1:def_12; ||.((g . (n + k1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) by A19; then ||.((g . m) - (g . n)).|| < e / 2 by A25, A28, XXREAL_0:2; hence ||.((g . l) - (g . m)).|| < e by A23, A30, Lm1; ::_thesis: verum end; hence for n, m being Element of NAT st n >= nn & m >= nn holds ||.((g . n) - (g . m)).|| < e ; ::_thesis: verum end; then g is Cauchy_sequence_by_Norm by RSSPACE3:8; then A31: g is convergent by LOPBAN_1:def_15; then A32: K (#) ||.(g - (lim g)).|| is convergent by NORMSP_1:24, SEQ_2:7; A33: lim (K (#) ||.(g - (lim g)).||) = K * (lim ||.(g - (lim g)).||) by A31, NORMSP_1:24, SEQ_2:8 .= K * 0 by A31, NORMSP_1:24 .= 0 ; A34: for e being Real st e > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e proof let e be Real; ::_thesis: ( e > 0 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e ) assume e > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e then consider n being Element of NAT such that A35: for m being Element of NAT st n <= m holds abs (((K (#) ||.(g - (lim g)).||) . m) - 0) < e by A32, A33, SEQ_2:def_7; take n ; ::_thesis: for m being Element of NAT st n <= m holds ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ ||.(((g_^\_1)_._m)_-_(f_._(lim_g))).||_<_e let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e ) assume n <= m ; ::_thesis: ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e then abs (((K (#) ||.(g - (lim g)).||) . m) - 0) < e by A35; then abs (K * (||.(g - (lim g)).|| . m)) < e by SEQ_1:9; then abs (K * ||.((g - (lim g)) . m).||) < e by NORMSP_0:def_4; then A36: abs (K * ||.((g . m) - (lim g)).||) < e by NORMSP_1:def_4; K * ||.((g . m) - (lim g)).|| <= abs (K * ||.((g . m) - (lim g)).||) by ABSVALUE:4; then A37: K * ||.((g . m) - (lim g)).|| < e by A36, XXREAL_0:2; ||.(((g ^\ 1) . m) - (f . (lim g))).|| <= K * ||.((g . m) - (lim g)).|| by A8; hence ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e by A37, XXREAL_0:2; ::_thesis: verum end; hence for m being Element of NAT st n <= m holds ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e ; ::_thesis: verum end; take xp = lim g; ::_thesis: ( f . xp = xp & ( for x being Point of X st f . x = x holds xp = x ) ) A38: ( g ^\ 1 is convergent & lim (g ^\ 1) = lim g ) by A31, LOPBAN_3:9; then A39: lim g = f . (lim g) by A34, NORMSP_1:def_7; now__::_thesis:_for_x_being_Point_of_X_st_f_._x_=_x_holds_ x_=_xp let x be Point of X; ::_thesis: ( f . x = x implies x = xp ) assume A40: f . x = x ; ::_thesis: x = xp A41: for k being Element of NAT holds ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power k) proof defpred S2[ Element of NAT ] means ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power \$1); A42: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume S2[k] ; ::_thesis: S2[k + 1] then A43: K * ||.(x - xp).|| <= K * (||.(x - xp).|| * (K to_power k)) by A1, XREAL_1:64; ||.((f . x) - (f . xp)).|| <= K * ||.(x - xp).|| by A3; then ||.((f . x) - (f . xp)).|| <= ||.(x - xp).|| * (K * (K to_power k)) by A43, XXREAL_0:2; then ||.((f . x) - (f . xp)).|| <= ||.(x - xp).|| * ((K to_power 1) * (K to_power k)) by POWER:25; hence S2[k + 1] by A1, A39, A40, POWER:27; ::_thesis: verum end; ||.(x - xp).|| = ||.(x - xp).|| * 1 .= ||.(x - xp).|| * (K to_power 0) by POWER:24 ; then A44: S2[ 0 ] ; for n being Element of NAT holds S2[n] from NAT_1:sch_1(A44, A42); hence for k being Element of NAT holds ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power k) ; ::_thesis: verum end; for e being Real st 0 < e holds ||.(x - xp).|| < e proof let e be Real; ::_thesis: ( 0 < e implies ||.(x - xp).|| < e ) assume 0 < e ; ::_thesis: ||.(x - xp).|| < e then consider n being Element of NAT such that A45: abs (||.(x - xp).|| * (K to_power n)) < e by A1, A2, Lm2; ||.(x - xp).|| * (K to_power n) <= abs (||.(x - xp).|| * (K to_power n)) by ABSVALUE:4; then A46: ||.(x - xp).|| * (K to_power n) < e by A45, XXREAL_0:2; ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power n) by A41; hence ||.(x - xp).|| < e by A46, XXREAL_0:2; ::_thesis: verum end; hence x = xp by Lm1; ::_thesis: verum end; hence ( f . xp = xp & ( for x being Point of X st f . x = x holds xp = x ) ) by A38, A34, NORMSP_1:def_7; ::_thesis: verum end; theorem :: NFCONT_2:15 for X being RealBanachSpace for f being Function of X,X st ex n0 being Element of NAT st iter (f,n0) is Contraction of X holds ex xp being Point of X st ( f . xp = xp & ( for x being Point of X st f . x = x holds xp = x ) ) proof let X be RealBanachSpace; ::_thesis: for f being Function of X,X st ex n0 being Element of NAT st iter (f,n0) is Contraction of X holds ex xp being Point of X st ( f . xp = xp & ( for x being Point of X st f . x = x holds xp = x ) ) let f be Function of X,X; ::_thesis: ( ex n0 being Element of NAT st iter (f,n0) is Contraction of X implies ex xp being Point of X st ( f . xp = xp & ( for x being Point of X st f . x = x holds xp = x ) ) ) given n0 being Element of NAT such that A1: iter (f,n0) is Contraction of X ; ::_thesis: ex xp being Point of X st ( f . xp = xp & ( for x being Point of X st f . x = x holds xp = x ) ) consider xp being Point of X such that A2: (iter (f,n0)) . xp = xp and A3: for x being Point of X st (iter (f,n0)) . x = x holds xp = x by A1, Th14; A4: now__::_thesis:_for_x_being_Point_of_X_st_f_._x_=_x_holds_ xp_=_x let x be Point of X; ::_thesis: ( f . x = x implies xp = x ) assume A5: f . x = x ; ::_thesis: xp = x for n being Element of NAT holds (iter (f,n)) . x = x proof defpred S1[ Element of NAT ] means (iter (f,\$1)) . x = x; A6: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A7: S1[n] ; ::_thesis: S1[n + 1] (iter (f,(n + 1))) . x = (f * (iter (f,n))) . x by FUNCT_7:71 .= x by A5, A7, FUNCT_2:15 ; hence S1[n + 1] ; ::_thesis: verum end; (iter (f,0)) . x = (id the carrier of X) . x by FUNCT_7:84 .= x by FUNCT_1:17 ; then A8: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A6); hence for n being Element of NAT holds (iter (f,n)) . x = x ; ::_thesis: verum end; then (iter (f,n0)) . x = x ; hence xp = x by A3; ::_thesis: verum end; (iter (f,n0)) . (f . xp) = ((iter (f,n0)) * f) . xp by FUNCT_2:15 .= (iter (f,(n0 + 1))) . xp by FUNCT_7:69 .= (f * (iter (f,n0))) . xp by FUNCT_7:71 .= f . xp by A2, FUNCT_2:15 ; then f . xp = xp by A3; hence ex xp being Point of X st ( f . xp = xp & ( for x being Point of X st f . x = x holds xp = x ) ) by A4; ::_thesis: verum end; theorem :: NFCONT_2:16 for K, L, e being real number st 0 < K & K < 1 & 0 < e holds ex n being Element of NAT st abs (L * (K to_power n)) < e by Lm2;