thus ( a is_a_fixpoint_of f implies a = f . a ) ; :: thesis: ( a = f . a implies a is_a_fixpoint_of f )
assume A1: a = f . a ; :: thesis: a is_a_fixpoint_of f
a in A ;
hence a in dom f by FUNCT_2:52; :: according to ABIAN:def 3 :: thesis: a = f . a
thus a = f . a by A1; :: thesis: verum