let X be RealBanachSpace; :: thesis: for f being Function of X,X st ex n0 being Nat st iter (f,n0) is contraction holds
f is with_unique_fixpoint
let f be Function of X,X; :: thesis: ( ex n0 being Nat st iter (f,n0) is contraction implies f is with_unique_fixpoint )
given n0 being Nat such that A1: iter (f,n0) is contraction ; :: thesis: f is with_unique_fixpoint
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, NFCONT_2:14;
take xp ; :: according to ORDEQ_01:def 1 :: thesis: ( xp is_a_fixpoint_of f & ( for y being set st y is_a_fixpoint_of f holds
xp = y ) )
thus A4: xp is_a_fixpoint_of f :: thesis: for y being set st y is_a_fixpoint_of f holds
xp = y

proof

A5: (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, FUNCT_2:15 ;
thus f . xp = xp by A5, A3; :: according to ABIAN:def 4 :: thesis: verum

end;

A6: 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 A7: f . x = x ; :: thesis: xp = x
for n being Nat holds (iter (f,n)) . x = x

proof

defpred S₁[ Nat] means (iter (f,$1)) . x = x;
(iter (f,0)) . x = (id the carrier of X) . x by FUNCT_7:84
.= x ;
then A8: S₁[ 0 ] ;

A9: 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 A10: S₁[n] ; :: thesis: S₁[n + 1]
reconsider m = n as Element of NAT by ORDINAL1:def 12;
(iter (f,(n + 1))) . x = (f * (iter (f,m))) . x by FUNCT_7:71
.= x by A7, A10, FUNCT_2:15 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A8, A9);
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;

let y be set ; :: thesis: ( y is_a_fixpoint_of f implies xp = y )
A11: dom f = the carrier of X by FUNCT_2:def 1;
assume A12: y is_a_fixpoint_of f ; :: thesis: xp = y
then reconsider x1 = xp, y1 = y as Point of X by A11;
A13: ( f . x1 = x1 & f . y1 = y1 ) by A12, A4;
thus xp = y by A6, A13; :: thesis: verum