let x be set ; :: thesis: for f being Function st x is_a_fixpoint_of f holds
x in rng f
let f be Function; :: thesis: ( x is_a_fixpoint_of f implies x in rng f )
assume ( x in dom f & x = f . x ) ; :: according to ABIAN:def 3 :: thesis: x in rng f
hence x in rng f by FUNCT_1:def 3; :: thesis: verum