:: deftheorem Def10 defines iteration_of MMLQUER2:def 10 :
for X being set
for O being Operation of X st O is co-well_founded & O is irreflexive & O is finite holds
for b₃ being Relation of X holds
( b₃ = iteration_of O iff ex f being Function of X,NAT st
( b₃ = value_of f & ( for x being Element of X st x in X holds
ex n being Nat st
( f . x = n & ( x . (iter (O,n)) <> {} or ( n = 0 & x . (iter (O,n)) = {} ) ) & x . (iter (O,(n + 1))) = {} ) ) ) );