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 5;
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:76;
A8: rng (iter f,n) c= X by A1, A2, FUNCT_7:76;
a in rng (iter f,n) by A1, A5, A6, A7, FUNCT_1:12;
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