A1: ( dom f = X & rng f c= X ) by FUNCT_2:def 1;
then A2: dom (A,g iter f) = dom f by 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
A3: ( b in dom (A,g iter f) & a = (A,g iter f) . b ) by FUNCT_1:def 5;
reconsider b = b as Element of X by A1, Def7, A3;

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, A3, 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
A4: ( (A,g iter f) . b = (iter f,n) . b & (iter f,n) . b nin A & ( for i being Nat st i < n holds
(iter f,i) . b in A ) ) by A1, Th10;
A5: n in NAT by ORDINAL1:def 13;
then dom (iter f,n) = dom f by A1, FUNCT_7:76;
then ( rng (iter f,n) c= X & a in rng (iter f,n) ) by A1, A3, A4, A5, FUNCT_1:12, FUNCT_7:76;
hence not a nin X ; :: thesis: verum

end;

end;

end;

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