let x, X be set ; :: thesis: 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
let f be Function of X,X; :: thesis: ( 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 ) ) implies x is_a_fixpoint_of f )
given n being Element of NAT such that A1: x is_a_fixpoint_of iter (f,n) and
A2: for y being set st y is_a_fixpoint_of iter (f,n) holds
x = y ; :: thesis: x is_a_fixpoint_of f
( dom f = X & dom (iter (f,n)) = X ) by FUNCT_2:52;
hence x in dom f by A1; :: according to ABIAN:def 3 :: thesis: x = f . x
thus x = f . x by A1, A2, Th2; :: thesis: verum