A1: dom f = X by FUNCT_2:def 1;
A2: rng f c= X ;
then A3: dom ((A,g) iter f) = dom f by A1, Def7;
rng ((A,g) iter f) c= X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( a nin rng ((A,g) iter f) or not a nin X )
assume a in rng ((A,g) iter f) ; :: thesis: not a nin X
then consider b being set such that
A4: b in dom ((A,g) iter f) and
A5: a = ((A,g) iter f) . b by FUNCT_1:def 3;
reconsider b = b as Element of X by A1, A2, A4, Def7;

per cases ( f orbit b c= A or not f orbit b c= A ) ;

suppose f orbit b c= A ; :: thesis: not a nin X

then a = g . b by A1, A2, A5, Def7;
hence not a nin X ; :: thesis: verum

end;

suppose not f orbit b c= A ; :: thesis: not a nin X

then consider n being Nat such that
A6: ((A,g) iter f) . b = (iter (f,n)) . b and
(iter (f,n)) . b nin A and
for i being Nat st i < n holds
(iter (f,i)) . b in A by A1, A2, Th10;
A7: dom (iter (f,n)) = dom f by A1, A2, FUNCT_7:74;
A8: rng (iter (f,n)) c= X by A1, A2, FUNCT_7:74;
a in rng (iter (f,n)) by A1, A5, A6, A7, FUNCT_1:3;
hence not a nin X by A8; :: thesis: verum

end;

end;

end;

hence (A,g) iter f is Element of Funcs (X,X) by A1, A3, FUNCT_2:def 2; :: thesis: verum