:: deftheorem defines is_a_fixpoint_of ABIAN:def 3 :
for x being object
for f being Function holds
( x is_a_fixpoint_of f iff ( x in dom f & x = f . x ) );