let X be RealBanachSpace; :: thesis: for f being Function of X,X st f 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: ( f 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 f 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 consider xp being set such that
A1: ( xp is_a_fixpoint_of f & ( for x being set st x is_a_fixpoint_of f holds
xp = x ) ) by Def1;
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