let X be RealBanachSpace; :: thesis: for S being non empty Subset of X
for f being PartFunc of X,X st S is closed & dom f = S & rng f c= S & ex k being Real st
( 0 < k & k < 1 & ( for x, y being Point of X st x in S & y in S holds
||.((f /. x) - (f /. y)).|| <= k * ||.(x - y).|| ) ) holds
( ex x0 being Point of X st
( x0 in S & f . x0 = x0 ) & ( for x0, y0 being Point of X st x0 in S & y0 in S & f . x0 = x0 & f . y0 = y0 holds
x0 = y0 ) )
let S be non empty Subset of X; :: thesis: for f being PartFunc of X,X st S is closed & dom f = S & rng f c= S & ex k being Real st
( 0 < k & k < 1 & ( for x, y being Point of X st x in S & y in S holds
||.((f /. x) - (f /. y)).|| <= k * ||.(x - y).|| ) ) holds
( ex x0 being Point of X st
( x0 in S & f . x0 = x0 ) & ( for x0, y0 being Point of X st x0 in S & y0 in S & f . x0 = x0 & f . y0 = y0 holds
x0 = y0 ) )
let f be PartFunc of X,X; :: thesis: ( S is closed & dom f = S & rng f c= S & ex k being Real st
( 0 < k & k < 1 & ( for x, y being Point of X st x in S & y in S holds
||.((f /. x) - (f /. y)).|| <= k * ||.(x - y).|| ) ) implies ( ex x0 being Point of X st
( x0 in S & f . x0 = x0 ) & ( for x0, y0 being Point of X st x0 in S & y0 in S & f . x0 = x0 & f . y0 = y0 holds
x0 = y0 ) ) )
assume that
A1: S is closed and
A2: ( dom f = S & rng f c= S ) and
A3: ex k being Real st
( 0 < k & k < 1 & ( for x, y being Point of X st x in S & y in S holds
||.((f /. x) - (f /. y)).|| <= k * ||.(x - y).|| ) ) ; :: thesis: ( ex x0 being Point of X st
( x0 in S & f . x0 = x0 ) & ( for x0, y0 being Point of X st x0 in S & y0 in S & f . x0 = x0 & f . y0 = y0 holds
x0 = y0 ) )
consider x0 being object such that
A4: x0 in S by XBOOLE_0:def 1;
reconsider x0 = x0 as Element of X by A4;
consider K being Real such that
A5: 0 < K and
A6: K < 1 and
A7: for x, y being Point of X st x in S & y in S holds
||.((f /. x) - (f /. y)).|| <= K * ||.(x - y).|| by A3;
deffunc H1( set , set ) -> set = f . $2;
consider g being Function such that
A8: ( dom g = NAT & g . 0 = x0 & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) ) from NAT_1:sch 11();
 defpred S1[ Nat] means ( g . $1 in S & g . $1 is Element of X );
A9: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A10: S1[k] ; :: thesis: S1[k + 1]
A11: g . (k + 1) = f . (g . k) by A8;
f . (g . k) in rng f by A2, A10, FUNCT_1:3;
hence S1[k + 1] by A2, A11; :: thesis: verum
end;
A12: S1[ 0 ] by A4, A8;
A13: for n being Nat holds S1[n] from NAT_1:sch 2(A12, A9);
 for n being object st n in NAT holds
g . n in the carrier of X
proof
let n be object ; :: thesis: ( n in NAT implies g . n in the carrier of X )
assume A14: n in NAT ; :: thesis: g . n in the carrier of X
reconsider k = n as Nat by A14;
g . k is Element of X by A13;
hence g . n in the carrier of X ; :: thesis: verum
end;
then reconsider g = g as sequence of X by A8, FUNCT_2:3;
for x being Element of NAT holds g . x in S by A13;
then A15: rng g c= S by FUNCT_2:114;
A16: for n being Nat holds ||.((g . (n + 1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power n)
proof
defpred S2[ Nat] means ||.((g . ($1 + 1)) - (g . $1)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power $1);
A17: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
A18: ( g . (k + 1) in S & g . k in S ) by A13;
A19: ( f /. (g . (k + 1)) = f . (g . (k + 1)) & f /. (g . k) = f . (g . k) ) by A2, A13, PARTFUN1:def 6;
assume S2[k] ; :: thesis: S2[k + 1]
then A20: K * ||.((g . (k + 1)) - (g . k)).|| <= K * (||.((g . 1) - (g . 0)).|| * (K to_power k)) by A5, XREAL_1:64;
||.((f /. (g . (k + 1))) - (f /. (g . k))).|| <= K * ||.((g . (k + 1)) - (g . k)).|| by A7, A18;
then ||.((f /. (g . (k + 1))) - (f /. (g . k))).|| <= ||.((g . 1) - (g . 0)).|| * (K * (K to_power k)) by A20, XXREAL_0:2;
then A21: ||.((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 A8;
then ||.((g . ((k + 1) + 1)) - (g . (k + 1))).|| = ||.((f /. (g . (k + 1))) - (f /. (g . k))).|| by A8, A19;
hence S2[k + 1] by A5, A21, 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 A22: S2[ 0 ] ;
for n being Nat holds S2[n] from NAT_1:sch 2(A22, A17);
 hence for n being Nat holds ||.((g . (n + 1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power n) ; :: thesis: verum
end;
A23: for k, n being 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[ Nat] means for n being Nat holds ||.((g . (n + $1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + $1))) / (1 - K));
A24: now :: thesis: for k being Nat st S2[k] holds
S2[k + 1]
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A25: S2[k] ; :: thesis: S2[k + 1]
now :: thesis: for n being 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 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 A6;
then A26: (||.((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 A5, 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 A16, A25;
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 A26, XXREAL_0:2; :: thesis: verum
end;
hence S2[k + 1] ; :: thesis: verum
end;
now :: thesis: for n being 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 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 ;
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 A27: S2[ 0 ] ;
for k being Nat holds S2[k] from NAT_1:sch 2(A27, A24);
 hence for k, n being 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;
A28: for k, n being Nat holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K))
proof
let k be Nat; :: thesis: for n being Nat holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K))
now :: thesis: for n being Nat holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K))
let n be Nat; :: thesis: ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K))
K to_power (n + k) > 0 by A5, POWER:34;
then A29: (K to_power n) - (K to_power (n + k)) <= (K to_power n) - 0 by XREAL_1:13;
1 - K > 1 - 1 by A6, XREAL_1:15;
then ((K to_power n) - (K to_power (n + k))) / (1 - K) <= (K to_power n) / (1 - K) by A29, XREAL_1:72;
then A30: ||.((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 A23;
hence ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) by A30, XXREAL_0:2; :: thesis: verum
end;
hence for n being 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 Nat st
for n, m being Nat st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < e
let e be Real; :: thesis: ( e > 0 implies ex nn being Nat st
for n, m being Nat st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < e )
assume A31: e > 0 ; :: thesis: ex nn being Nat st
for n, m being Nat st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < e
e / 2 > 0 by A31, XREAL_1:215;
then consider n being Nat such that
A32: |.((||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n)).| < e / 2 by A5, A6, NFCONT_2:16;
reconsider nn = n + 1 as Nat ;
take nn = nn; :: thesis: for n, m being Nat st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < e
(||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n) <= |.((||.((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 A32, XXREAL_0:2;
then A33: ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) < e / 2 by XCMPLX_1:75;
now :: thesis: for m, l being Nat st nn <= m & nn <= l holds
||.((g . l) - (g . m)).|| < e
let m, l be Nat; :: thesis: ( nn <= m & nn <= l implies ||.((g . l) - (g . m)).|| < e )
assume that
A34: nn <= m and
A35: nn <= l ; :: thesis: ||.((g . l) - (g . m)).|| < e
n < m by A34, NAT_1:13;
then consider k1 being Nat such that
A36: n + k1 = m by NAT_1:10;
n < l by A35, NAT_1:13;
then consider k2 being Nat such that
A37: n + k2 = l by NAT_1:10;
reconsider k2 = k2 as Nat ;
||.((g . (n + k2)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) by A28;
then A38: ||.((g . l) - (g . n)).|| < e / 2 by A33, A37, XXREAL_0:2;
reconsider k1 = k1 as Nat ;
||.((g . (n + k1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) by A28;
then ||.((g . m) - (g . n)).|| < e / 2 by A33, A36, XXREAL_0:2;
hence ||.((g . l) - (g . m)).|| < e by A31, A38, NDIFF_2:4; :: thesis: verum
end;
hence for n, m being Nat st n >= nn & m >= nn holds
||.((g . n) - (g . m)).|| < e ; :: thesis: verum
end;
then A39: g is convergent by LOPBAN_1:def 15, RSSPACE3:8;
then A40: K (#) ||.(g - (lim g)).|| is convergent by NORMSP_1:24, SEQ_2:7;
A41: lim g in S by A1, A15, A39, NFCONT_1:def 3;
A42: now :: thesis: for n being Nat holds ||.(((g ^\ 1) . n) - (f /. (lim g))).|| <= K * ||.((g . n) - (lim g)).||
let n be Nat; :: thesis: ||.(((g ^\ 1) . n) - (f /. (lim g))).|| <= K * ||.((g . n) - (lim g)).||
A43: g . n in S by A13;
A44: ( f /. (g . n) = f . (g . n) & f /. (lim g) = f . (lim g) ) by A1, A2, A13, A15, A39, NFCONT_1:def 3, PARTFUN1:def 6;
||.(((g ^\ 1) . n) - (f /. (lim g))).|| = ||.((g . (n + 1)) - (f /. (lim g))).|| by NAT_1:def 3
.= ||.((f /. (g . n)) - (f /. (lim g))).|| by A8, A44 ;
hence ||.(((g ^\ 1) . n) - (f /. (lim g))).|| <= K * ||.((g . n) - (lim g)).|| by A7, A41, A43; :: thesis: verum
end;
A45: lim (K (#) ||.(g - (lim g)).||) = K * (lim ||.(g - (lim g)).||) by A39, NORMSP_1:24, SEQ_2:8
.= K * 0 by A39, NORMSP_1:24
.= 0 ;
A46: for e being Real st e > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((g ^\ 1) . m) - (f /. (lim g))).|| < e
proof
let e be Real; :: thesis: ( e > 0 implies ex n being Nat st
for m being Nat st n <= m holds
||.(((g ^\ 1) . m) - (f /. (lim g))).|| < e )
assume e > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.(((g ^\ 1) . m) - (f /. (lim g))).|| < e
then consider n being Nat such that
A47: for m being Nat st n <= m holds
|.(((K (#) ||.(g - (lim g)).||) . m) - 0).| < e by A40, A45, SEQ_2:def 7;
take n ; :: thesis: for m being Nat st n <= m holds
||.(((g ^\ 1) . m) - (f /. (lim g))).|| < e
now :: thesis: for m being Nat st n <= m holds
||.(((g ^\ 1) . m) - (f /. (lim g))).|| < e
let m be Nat; :: thesis: ( n <= m implies ||.(((g ^\ 1) . m) - (f /. (lim g))).|| < e )
assume n <= m ; :: thesis: ||.(((g ^\ 1) . m) - (f /. (lim g))).|| < e
then |.(((K (#) ||.(g - (lim g)).||) . m) - 0).| < e by A47;
then |.(K * (||.(g - (lim g)).|| . m)).| < e by SEQ_1:9;
then |.(K * ||.((g - (lim g)) . m).||).| < e by NORMSP_0:def 4;
then A48: |.(K * ||.((g . m) - (lim g)).||).| < e by NORMSP_1:def 4;
K * ||.((g . m) - (lim g)).|| <= |.(K * ||.((g . m) - (lim g)).||).| by ABSVALUE:4;
then A49: K * ||.((g . m) - (lim g)).|| < e by A48, XXREAL_0:2;
||.(((g ^\ 1) . m) - (f /. (lim g))).|| <= K * ||.((g . m) - (lim g)).|| by A42;
hence ||.(((g ^\ 1) . m) - (f /. (lim g))).|| < e by A49, XXREAL_0:2; :: thesis: verum
end;
hence for m being Nat st n <= m holds
||.(((g ^\ 1) . m) - (f /. (lim g))).|| < e ; :: thesis: verum
end;
set xp = lim g;
A50: ( g ^\ 1 is convergent & lim (g ^\ 1) = lim g ) by A39, LOPBAN_3:9;
then A51: lim g = f /. (lim g) by A46, NORMSP_1:def 7;
A52: now :: thesis: for x being Point of X st x in S & f . x = x holds
x = lim g
let x be Point of X; :: thesis: ( x in S & f . x = x implies x = lim g )
assume A53: ( x in S & f . x = x ) ; :: thesis: x = lim g
A54: f /. x = x by A2, A53, PARTFUN1:def 6;
A55: for k being Nat holds ||.(x - (lim g)).|| <= ||.(x - (lim g)).|| * (K to_power k)
proof
defpred S2[ Nat] means ||.(x - (lim g)).|| <= ||.(x - (lim g)).|| * (K to_power $1);
A56: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume S2[k] ; :: thesis: S2[k + 1]
then A57: K * ||.(x - (lim g)).|| <= K * (||.(x - (lim g)).|| * (K to_power k)) by A5, XREAL_1:64;
||.((f /. x) - (f /. (lim g))).|| <= K * ||.(x - (lim g)).|| by A7, A41, A53;
then ||.((f /. x) - (f /. (lim g))).|| <= ||.(x - (lim g)).|| * (K * (K to_power k)) by A57, XXREAL_0:2;
then ||.((f /. x) - (f /. (lim g))).|| <= ||.(x - (lim g)).|| * ((K to_power 1) * (K to_power k)) by POWER:25;
hence S2[k + 1] by A5, A51, A54, POWER:27; :: thesis: verum
end;
||.(x - (lim g)).|| = ||.(x - (lim g)).|| * 1
.= ||.(x - (lim g)).|| * (K to_power 0) by POWER:24 ;
then A58: S2[ 0 ] ;
for n being Nat holds S2[n] from NAT_1:sch 2(A58, A56);
 hence for k being Nat holds ||.(x - (lim g)).|| <= ||.(x - (lim g)).|| * (K to_power k) ; :: thesis: verum
end;
for e being Real st 0 < e holds
||.(x - (lim g)).|| < e
proof
let e be Real; :: thesis: ( 0 < e implies ||.(x - (lim g)).|| < e )
assume 0 < e ; :: thesis: ||.(x - (lim g)).|| < e
then consider n being Nat such that
A59: |.(||.(x - (lim g)).|| * (K to_power n)).| < e by A5, A6, NFCONT_2:16;
||.(x - (lim g)).|| * (K to_power n) <= |.(||.(x - (lim g)).|| * (K to_power n)).| by ABSVALUE:4;
then A60: ||.(x - (lim g)).|| * (K to_power n) < e by A59, XXREAL_0:2;
||.(x - (lim g)).|| <= ||.(x - (lim g)).|| * (K to_power n) by A55;
hence ||.(x - (lim g)).|| < e by A60, XXREAL_0:2; :: thesis: verum
end;
hence x = lim g by NDIFF_2:4; :: thesis: verum
end;
lim g = f /. (lim g) by A46, A50, NORMSP_1:def 7;
then lim g = f . (lim g) by A1, A2, A15, A39, NFCONT_1:def 3, PARTFUN1:def 6;
hence ex x0 being Point of X st
( x0 in S & f . x0 = x0 ) by A1, A15, A39, NFCONT_1:def 3; :: thesis: for x0, y0 being Point of X st x0 in S & y0 in S & f . x0 = x0 & f . y0 = y0 holds
x0 = y0
for x0, y0 being Point of X st x0 in S & y0 in S & f . x0 = x0 & f . y0 = y0 holds
x0 = y0
proof
let x0, y0 be Point of X; :: thesis: ( x0 in S & y0 in S & f . x0 = x0 & f . y0 = y0 implies x0 = y0 )
assume that
A61: x0 in S and
A62: y0 in S and
A63: f . x0 = x0 and
A64: f . y0 = y0 ; :: thesis: x0 = y0
x0 = lim g by A52, A61, A63;
hence x0 = y0 by A52, A62, A64; :: thesis: verum
end;
hence for x0, y0 being Point of X st x0 in S & y0 in S & f . x0 = x0 & f . y0 = y0 holds
x0 = y0 ; :: thesis: verum