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 ;
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 Nat holds (iter (f,n)) . x = x
proof
defpred S1[ Nat] means (iter (f,\$1)) . x = x;
A6: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; :: thesis: S1[n + 1]
(iter (f,(n + 1))) . x = (f * (iter (f,n))) . x by FUNCT_7:71
.= x by ;
hence S1[n + 1] ; :: thesis: verum
end;
(iter (f,0)) . x = (id the carrier of X) . x by FUNCT_7:84
.= x ;
then A8: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A8, A6);
hence for n being Nat holds (iter (f,n)) . x = x ; :: thesis: verum
end;
then (iter (f,n0)) . x = x ;
hence xp = x by A3; :: thesis: verum
end;
(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 ;
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