for x, X being set
for f being Function of X,X st ex n being Element of NAT st
( x is_a_fixpoint_of iter (f,n) & ( for y being set st y is_a_fixpoint_of iter (f,n) holds
x = y ) ) holds
x is_a_fixpoint_of f