:: deftheorem defines iter AOFA_000:def 6 :
for f being Function st rng f c= dom f holds
for A, x being set
for b₄ being Function holds
( b₄ = (A,x) 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 = x ) & ( 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 ) ) ) ) );