let X be RealBanachSpace; :: thesis: for f being Function of X,X st ex n0 being Element of NAT st iter (f,n0) is contraction 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 implies ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) ) )
assume ex n0 being Element of NAT st iter (f,n0) is contraction ; :: thesis: ex xp being Point of X st
( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
then f is with_unique_fixpoint by Th7;
then consider xp being set such that
A1: ( xp is_a_fixpoint_of f & ( for y being set st y is_a_fixpoint_of f holds
xp = y ) ) ;
xp in dom f by A1;
then reconsider xp = xp as Point of X ;
take xp ; :: thesis: ( f . xp = xp & ( for x being Point of X st f . x = x holds
xp = x ) )
thus f . xp = xp by A1; :: 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 f . x = x ; :: thesis: xp = x
then x is_a_fixpoint_of f ;
hence xp = x by A1; :: thesis: verum