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 ) )
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 Def7;
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 A6, FUNCT_2:5; :: 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 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 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 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) + 1) = f . (g . (k + 1)) & 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 Nat holds S2[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 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[ 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 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 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))) + ((1 * (K to_power (n + k))) - (K * (K to_power (n + 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 CLVECT_1:111, 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 CLVECT_1:102 ;
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 NAT_1:sch 2(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))
A20: 0 <= ||.((g . 1) - (g . 0)).|| by CLVECT_1:105;
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 A20, 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 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 A23: 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 A23;
then consider n being Nat such that
A24: |.((||.((g . 1) - (g . 0)).|| / (1 - K)) * (K to_power n)).| < e / 2 by A1, A2, 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 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 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
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 Nat ;
A30: n in NAT by ORDINAL1:def 12;
A31: k2 in NAT by ORDINAL1:def 12;
||.((g . (n + k2)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K)) by A19, A30, A31;
then A32: ||.((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, A30;
then ||.((g . m) - (g . n)).|| < e / 2 by A25, A28, XXREAL_0:2;
hence ||.((g . l) - (g . m)).|| < e by A32, Lm2; :: 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 CSSPACE3:8;
then A33: g is convergent by CLOPBAN1:def 13;
then A34: K (#) ||.(g - (lim g)).|| is convergent by CLVECT_1:118, SEQ_2:7;
A35: lim (K (#) ||.(g - (lim g)).||) = K * (lim ||.(g - (lim g)).||) by A33, CLVECT_1:118, SEQ_2:8
.= K * 0 by A33, CLVECT_1:118
.= 0 ;
A36: 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
A37: for m being Nat st n <= m holds
|.(((K (#) ||.(g - (lim g)).||) . m) - 0).| < e by A34, A35, 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 )
A38: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e
then |.(((K (#) ||.(g - (lim g)).||) . m) - 0).| < e by A37;
then |.(K * (||.(g - (lim g)).|| . m)).| < e by SEQ_1:9;
then |.(K * ||.((g - (lim g)) . m).||).| < e by NORMSP_0:def 4;
then A39: |.(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 A40: K * ||.((g . m) - (lim g)).|| < e by A39, XXREAL_0:2;
||.(((g ^\ 1) . m) - (f . (lim g))).|| <= K * ||.((g . m) - (lim g)).|| by A8, A38;
hence ||.(((g ^\ 1) . m) - (f . (lim g))).|| < e by A40, 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 ) )
A41: ( g ^\ 1 is convergent & lim (g ^\ 1) = lim g ) by A33, CLOPBAN3:9;
then A42: lim g = f . (lim g) by A36, CLVECT_1:def 16;
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 A43: f . x = x ; :: thesis: x = xp
A44: for k being Element of NAT holds ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power k)
proof
defpred S2[ Nat] means ||.(x - xp).|| <= ||.(x - xp).|| * (K to_power $1);
A45: 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 A46: 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 A46, 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, A42, A43, POWER:27; :: thesis: verum
end;
||.(x - xp).|| = ||.(x - xp).|| * 1
.= ||.(x - xp).|| * (K to_power 0) by POWER:24 ;
then A47: S2[ 0 ] ;
for n being Nat holds S2[n] from NAT_1:sch 2(A47, A45);
 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 Nat such that
A48: |.(||.(x - xp).|| * (K to_power n)).| < e by A1, A2, NFCONT_2:16;
A49: n in NAT by ORDINAL1:def 12;
||.(x - xp).|| * (K to_power n) <= |.(||.(x - xp).|| * (K to_power n)).| by ABSVALUE:4;
then A50: ||.(x - xp).|| * (K to_power n) < e by A48, XXREAL_0:2;
||.(x - xp).|| <= ||.(x - xp).|| * (K to_power n) by A44, A49;
hence ||.(x - xp).|| < e by A50, 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 A41, A36, CLVECT_1:def 16; :: thesis: verum