let X be RealBanachSpace; 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; ( 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
; 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;
( S1[k] implies S1[k + 1] )
assume A6:
S1[
k]
;
S1[k + 1]
g . (k + 1) = f . (g . k)
by A4;
hence
S1[
k + 1]
by A6, FUNCT_2:5;
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;
A9:
for n being Nat holds ||.((g . (n + 1)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * (K to_power n)
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))
A19:
for k, n being Nat holds ||.((g . (n + k)) - (g . n)).|| <= ||.((g . 1) - (g . 0)).|| * ((K to_power n) / (1 - K))
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
take xp = lim g; ( 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 for x being Point of X st f . x = x holds
x = xpend;
hence
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
by A37, A33, NORMSP_1:def 7; verum