let X be RealBanachSpace; :: thesis: for f being Function of X,X st ex n0 being Nat st iter (f,n0) 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 ) )

let f be Function of X,X; :: thesis: ( ex n0 being Nat st iter (f,n0) 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 ) ) )

given n0 being Nat such that A1: iter (f,n0) 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 ) )

consider xp being Point of X such that

A2: (iter (f,n0)) . xp = xp and

A3: for x being Point of X st (iter (f,n0)) . x = x holds

xp = x by A1, Th14;

.= (iter (f,(n0 + 1))) . xp by FUNCT_7:69

.= (f * (iter (f,n0))) . xp by FUNCT_7:71

.= f . xp by A2, FUNCT_2:15 ;

then f . xp = xp by A3;

hence ex xp being Point of X st

( f . xp = xp & ( for x being Point of X st f . x = x holds

xp = x ) ) by A4; :: thesis: verum

ex xp being Point of X st

( f . xp = xp & ( for x being Point of X st f . x = x holds

xp = x ) )

let f be Function of X,X; :: thesis: ( ex n0 being Nat st iter (f,n0) 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 ) ) )

given n0 being Nat such that A1: iter (f,n0) 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 ) )

consider xp being Point of X such that

A2: (iter (f,n0)) . xp = xp and

A3: for x being Point of X st (iter (f,n0)) . x = x holds

xp = x by A1, Th14;

A4: now :: thesis: for x being Point of X st f . x = x holds

xp = x

(iter (f,n0)) . (f . xp) =
((iter (f,n0)) * f) . xp
by FUNCT_2:15
xp = x

let x be Point of X; :: thesis: ( f . x = x implies xp = x )

assume A5: f . x = x ; :: thesis: xp = x

for n being Nat holds (iter (f,n)) . x = x

hence xp = x by A3; :: thesis: verum

end;assume A5: f . x = x ; :: thesis: xp = x

for n being Nat holds (iter (f,n)) . x = x

proof

then
(iter (f,n0)) . x = x
;
defpred S_{1}[ Nat] means (iter (f,$1)) . x = x;

.= x ;

then A8: S_{1}[ 0 ]
;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A8, A6);

hence for n being Nat holds (iter (f,n)) . x = x ; :: thesis: verum

end;A6: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

(iter (f,0)) . x =
(id the carrier of X) . x
by FUNCT_7:84
S

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A7: S_{1}[n]
; :: thesis: S_{1}[n + 1]

(iter (f,(n + 1))) . x = (f * (iter (f,n))) . x by FUNCT_7:71

.= x by A5, A7, FUNCT_2:15 ;

hence S_{1}[n + 1]
; :: thesis: verum

end;assume A7: S

(iter (f,(n + 1))) . x = (f * (iter (f,n))) . x by FUNCT_7:71

.= x by A5, A7, FUNCT_2:15 ;

hence S

.= x ;

then A8: S

for n being Nat holds S

hence for n being Nat holds (iter (f,n)) . x = x ; :: thesis: verum

hence xp = x by A3; :: thesis: verum

.= (iter (f,(n0 + 1))) . xp by FUNCT_7:69

.= (f * (iter (f,n0))) . xp by FUNCT_7:71

.= f . xp by A2, FUNCT_2:15 ;

then f . xp = xp by A3;

hence ex xp being Point of X st

( f . xp = xp & ( for x being Point of X st f . x = x holds

xp = x ) ) by A4; :: thesis: verum