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 H₁( 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) = H₁(n,g . n) ) ) from NAT_1:sch 11();
defpred S₁[ Nat] means g . $1 in the carrier of X;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
g . (k + 1) = f . (g . k) by A4;
hence S₁[k + 1] by A6, FUNCT_2:5; :: thesis: verum

end;

A7: S₁[ 0 ] by A4;
for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A5);
then for n being object 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 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)).||
||.(((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 Nat holds ||.((g . (n + 1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power n)

proof

defpred S₂[ Nat] means ||.((g . ($1 + 1)) - (g . $1)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power $1);
A10: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume S₂[k] ; :: thesis: S₂[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 S₂[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: S₂[ 0 ] ;
for n being Nat holds S₂[n] from NAT_1:sch 2(A13, A10);
hence for n being Nat holds ||.((g . (n + 1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power n) ; :: thesis: verum

end;

A14: 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 S₂[ 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));

A15: now :: thesis: for k being Nat st S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A16: S₂[k] ; :: thesis: S₂[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 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 S₂[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 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: S₂[ 0 ] ;
for k being Nat holds S₂[k] from NAT_1:sch 2(A18, A15);
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;

A19: 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 A1, POWER:34;
then A20: (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 A20, XREAL_1:72;
then A21: ||.((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 A21, 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 A22: 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 A22, XREAL_1:215;
then consider n being Nat such that
A23: |.((||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n)).| < e / 2 by A1, A2, Lm2;
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 A23, XXREAL_0:2;
then A24: ||.((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
A25: nn <= m and
A26: nn <= l ; :: thesis: ||.((g . l) - (g . m)).|| < e
n < m by A25, NAT_1:13;
then consider k1 being Nat such that
A27: n + k1 = m by NAT_1:10;
n < l by A26, NAT_1:13;
then consider k2 being Nat such that
A28: 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 A19;
then A29: ||.((g . l) - (g . n)).|| < e / 2 by A24, A28, XXREAL_0:2;
reconsider k1 = k1 as Nat ;
||.((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 A24, A27, XXREAL_0:2;
hence ||.((g . l) - (g . m)).|| < e by A22, A29, Lm1; :: thesis: verum

end;

hence for n, m being 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 A30: g is convergent by LOPBAN_1:def 15;
then A31: K (#) ||.(g - (lim g)).|| is convergent by NORMSP_1:24, SEQ_2:7;
A32: lim (K (#) ||.(g - (lim g)).||) = K * (lim ||.(g - (lim g)).||) by A30, NORMSP_1:24, SEQ_2:8
.= K * 0 by A30, NORMSP_1:24
.= 0 ;
A33: 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
A34: for m being Nat st n <= m holds
|.(((K (#) ||.(g - (lim g)).||) . m) - 0).| < e by A31, A32, 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 A34;
then |.(K * (||.(g - (lim g)).|| . m)).| < e by SEQ_1:9;
then |.(K * ||.((g - (lim g)) . m).||).| < e by NORMSP_0:def 4;
then A35: |.(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 A36: K * ||.((g . m) - (lim g)).|| < e by A35, 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 A36, 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;

take xp = lim g; :: thesis: ( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
A37: ( g ^\ 1 is convergent & lim (g ^\ 1) = lim g ) by A30, LOPBAN_3:9;
then A38: lim g = f . (lim g) by A33, 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 A39: f . x = x ; :: thesis: x = xp
A40: for k being Nat holds ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power k)

proof

defpred S₂[ Nat] means ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power $1);
A41: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume S₂[k] ; :: thesis: S₂[k + 1]
then A42: 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 A42, XXREAL_0:2;
then ||.((f . x) - (f . xp)).|| <= ||.(x - xp).|| * ((K to_power 1) * (K to_power k)) by POWER:25;
hence S₂[k + 1] by A1, A38, A39, POWER:27; :: thesis: verum

end;

||.(x - xp).|| = ||.(x - xp).|| * 1
.= ||.(x - xp).|| * (K to_power 0) by POWER:24 ;
then A43: S₂[ 0 ] ;
for n being Nat holds S₂[n] from NAT_1:sch 2(A43, A41);
hence for k being 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 Nat such that
A44: |.(||.(x - xp).|| * (K to_power n)).| < e by A1, A2, Lm2;
||.(x - xp).|| * (K to_power n) <= |.(||.(x - xp).|| * (K to_power n)).| by ABSVALUE:4;
then A45: ||.(x - xp).|| * (K to_power n) < e by A44, XXREAL_0:2;
||.(x - xp).|| <= ||.(x - xp).|| * (K to_power n) by A40;
hence ||.(x - xp).|| < e by A45, 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 A37, A33, NORMSP_1:def 7; :: thesis: verum