let X be ComplexBanachSpace; :: thesis: for f being Function of X,X st ex n0 being Element of 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 Element of 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 Element of 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, Th40;

A4: now :: thesis: for x being Point of X st f . x = x holds
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 Element of NAT holds (iter (f,n)) . x = x

proof

defpred S₁[ Nat] means (iter (f,$1)) . x = x;

A6: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
A8: iter (f,n) is Function of X,X by FUNCT_7:83;
(iter (f,(n + 1))) . x = (f * (iter (f,n))) . x by FUNCT_7:71
.= x by A5, A7, A8, FUNCT_2:15 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(iter (f,0)) . x = (id the carrier of X) . x by FUNCT_7:84
.= x ;
then A9: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A9, A6);
hence for n being Element of NAT holds (iter (f,n)) . x = x ; :: thesis: verum

end;

then (iter (f,n0)) . x = x ;
hence xp = x by A3; :: thesis: verum

end;

A10: iter (f,n0) is Function of X,X by FUNCT_7:83;
(iter (f,n0)) . (f . xp) = ((iter (f,n0)) * f) . xp by FUNCT_2:15
.= (iter (f,(n0 + 1))) . xp by FUNCT_7:69
.= (f * (iter (f,n0))) . xp by FUNCT_7:71
.= f . xp by A2, A10, 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