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

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₁[ Element of NAT ] means (iter f,$1) . x = x;

A6: now

let n be Element of 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:85;
(iter f,(n + 1)) . x = (f * (iter f,n)) . x by FUNCT_7:73
.= x by A5, A7, A8, FUNCT_2:21 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(iter f,0 ) . x = (id the carrier of X) . x by FUNCT_7:86
.= x by FUNCT_1:34 ;
then A9: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(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:85;
(iter f,n0) . (f . xp) = ((iter f,n0) * f) . xp by FUNCT_2:21
.= (iter f,(n0 + 1)) . xp by FUNCT_7:71
.= (f * (iter f,n0)) . xp by FUNCT_7:73
.= f . xp by A2, A10, FUNCT_2:21 ;
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