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[ Nat] means g . \$1 in the carrier of X;
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be 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 ; :: thesis: verum
end;
A7: S1[ 0 ] by A4;
for n being Nat holds S1[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 ;
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 S2[ Nat] means ||.((g . (\$1 + 1)) - (g . \$1)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power \$1);
A10: 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 A11: K * ||.((g . (k + 1)) - (g . k)).|| <= K * (||.((g . 1) - (g . 0)).|| * (K to_power k)) by ;
||.((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 ;
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 ; :: thesis: verum
end;
||.((g . (0 + 1)) - (g . 0)).|| = ||.((g . 1) - (g . 0)).|| * 1
.= ||.((g . 1) - (g . 0)).|| * () by POWER:24 ;
then A13: S2[ 0 ] ;
for n being Nat holds S2[n] from 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 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));
A15: 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 A16: 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 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 ;
( ||.((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 ;
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 ;
hence ||.((g . (n + (k + 1))) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power (n + (k + 1)))) / (1 - K)) by ; :: 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 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 Nat holds S2[k] from 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 ;
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 ;
then ((K to_power n) - (K to_power (n + k))) / (1 - K) <= (K to_power n) / (1 - K) by ;
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 ; :: 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 ;
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 ;
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 ;
then consider k1 being Nat such that
A27: n + k1 = m by NAT_1:10;
n < l by ;
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 ;
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 ;
hence ||.((g . l) - (g . m)).|| < e by ; :: 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 ;
A32: lim (K (#) ||.(g - (lim g)).||) = K * (lim ||.(g - (lim g)).||) by
.= K * 0 by
.= 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 ;
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 ;
||.(((g ^\ 1) . m) - (f . (lim g))).|| <= K * ||.((g . m) - (lim g)).|| by A8;
hence ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e by ; :: 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 ;
then A38: lim g = f . (lim g) by ;
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 S2[ Nat] means ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power \$1);
A41: 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 A42: K * ||.(x - xp).|| <= K * (||.(x - xp).|| * (K to_power k)) by ;
||.((f . x) - (f . xp)).|| <= K * ||.(x - xp).|| by A3;
then ||.((f . x) - (f . xp)).|| <= ||.(x - xp).|| * (K * (K to_power k)) by ;
then ||.((f . x) - (f . xp)).|| <= ||.(x - xp).|| * ((K to_power 1) * (K to_power k)) by POWER:25;
hence S2[k + 1] by ; :: thesis: verum
end;
||.(x - xp).|| = ||.(x - xp).|| * 1
.= ||.(x - xp).|| * () by POWER:24 ;
then A43: S2[ 0 ] ;
for n being Nat holds S2[n] from 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 ;
||.(x - xp).|| <= ||.(x - xp).|| * (K to_power n) by A40;
hence ||.(x - xp).|| < e by ; :: 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 ; :: thesis: verum