theorem Th10: :: AOFA_000:10

for f, g being Function
for a, A being set st rng f c= dom f & a in dom f & not f orbit a c= A holds
ex n being Nat st
( ((A,g) iter f) . a = (iter (f,n)) . a & (iter (f,n)) . a nin A & ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) )