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