let X be ComplexBanachSpace; :: 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 ) )
consider x0 being 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 Def7;
deffunc H₁( set , set ) -> set = f . $2;
consider g being Function such that
A4: ( dom g = NAT & g . 0 = x0 & ( for n being Nat holds g . (n + 1) = H₁(n,g . n) ) ) from NAT_1:sch 11();
defpred S₁[ Element of NAT ] means g . $1 in the carrier of X;
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of 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:7; :: thesis: verum

end;

A7: S₁[ 0 ] by A4;
for n being Element of NAT holds S₁[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:5;

A8: now

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 S₂[ 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 S₂[k] holds
S₂[k + 1]

proof

let k be Element of 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:66;
||.((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:30;
( g . ((k + 1) + 1) = f . (g . (k + 1)) & g . (k + 1) = f . (g . k) ) by A4;
hence S₂[k + 1] by A1, A12, POWER:32; :: thesis: verum

end;

||.((g . (0 + 1)) - (g . 0)).|| = ||.((g . 1) - (g . 0)).|| * 1
.= ||.((g . 1) - (g . 0)).|| * (K to_power 0) by POWER:29 ;
then A13: S₂[ 0 ] ;
for n being Element of NAT holds S₂[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 S₂[ 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

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A16: S₂[k] ; :: thesis: S₂[k + 1]

now

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:90
.= (||.((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:75
.= ||.((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))) + ((1 * (K to_power (n + k))) - (K * (K to_power (n + k))))) / (1 - K)) by XCMPLX_1:63
.= ||.((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:30
.= ||.((g . 1) - (g . 0)).|| * (((K to_power n) - (K to_power ((n + k) + 1))) / (1 - K)) by A1, POWER:32 ;
( ||.((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 CLVECT_1:112, XREAL_1:9;
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

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:28
.= 0 by CLVECT_1:103 ;
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 Element of NAT holds S₂[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

let n be Element of NAT ; :: thesis: ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K))
A20: 0 <= ||.((g . 1) - (g . 0)).|| by CLVECT_1:106;
K to_power (n + k) > 0 by A1, POWER:39;
then A21: (K to_power n) - (K to_power (n + k)) <= (K to_power n) - 0 by XREAL_1:15;
1 - K > 1 - 1 by A2, XREAL_1:17;
then ((K to_power n) - (K to_power (n + k))) / (1 - K) <= (K to_power n) / (1 - K) by A21, XREAL_1:74;
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 A20, XREAL_1:66;
||.((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

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:217;
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, NFCONT_2:16;
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:11;
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:76;

now

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 13;
||.((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 13;
||.((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 A30, Lm2; :: 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 CCauchy by CSSPACE3:10;
then A31: g is convergent by CLOPBAN1:def 14;
then A32: K (#) ||.(g - (lim g)).|| is convergent by CLVECT_1:120, SEQ_2:21;
A33: lim (K (#) ||.(g - (lim g)).||) = K * (lim ||.(g - (lim g)).||) by A31, CLVECT_1:120, SEQ_2:22
.= K * 0 by A31, CLVECT_1:120
.= 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

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:13;
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 7;
K * ||.((g . m) - (lim g)).|| <= abs (K * ||.((g . m) - (lim g)).||) by ABSVALUE:11;
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, CLOPBAN3:13;
then A39: lim g = f . (lim g) by A34, CLVECT_1:def 18;

now

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 S₂[ Element of NAT ] means ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power $1);
A42: for k being Element of NAT st S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume S₂[k] ; :: thesis: S₂[k + 1]
then A43: K * ||.(x - xp).|| <= K * (||.(x - xp).|| * (K to_power k)) by A1, XREAL_1:66;
||.((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:30;
hence S₂[k + 1] by A1, A39, A40, POWER:32; :: thesis: verum

end;

||.(x - xp).|| = ||.(x - xp).|| * 1
.= ||.(x - xp).|| * (K to_power 0) by POWER:29 ;
then A44: S₂[ 0 ] ;
for n being Element of NAT holds S₂[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, NFCONT_2:16;
||.(x - xp).|| * (K to_power n) <= abs (||.(x - xp).|| * (K to_power n)) by ABSVALUE:11;
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 Lm4; :: thesis: verum

end;

hence ( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) ) by A38, A34, CLVECT_1:def 18; :: thesis: verum