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

( 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