let f be Function of X,X; :: thesis: ( f is contraction implies f is with_unique_fixpoint )
assume f is contraction ; :: thesis: f is with_unique_fixpoint
then consider xp being Point of X such that
A1: f . xp = xp and
A2: for x being Point of X st f . x = x holds
xp = x by 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 f . xp = xp by A1; :: according to ABIAN:def 4 :: thesis: for y being set st y is_a_fixpoint_of f holds
xp = y
let y be set ; :: thesis: ( y is_a_fixpoint_of f implies xp = y )
assume y is_a_fixpoint_of f ; :: thesis: xp = y
then ( y in dom f & f . y = y ) ;
hence xp = y by A2; :: thesis: verum