:: deftheorem Def7 defines iter AOFA_000:def 7 :
for f being Function st rng f c= dom f holds
for A being set
for g, b₄ being Function holds
( b₄ = (A,g) iter f iff ( dom b₄ = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b₄ . a = g . a ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
b₄ . a = (iter (f,n)) . a ) ) ) ) );