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
object ;
TARSKI:def 3 ( a nin rng ((A,g) iter f) or not a nin X )
assume
a in rng ((A,g) iter f)
;
not a nin X
then consider b being
object 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
not
f orbit b c= A
;
not a nin Xthen 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;
a in rng (iter (f,n))
by A1, A5, A6, A7, FUNCT_1:3;
hence
not
a nin X
;
verum end; end;
end;
hence
(A,g) iter f is Element of Funcs (X,X)
by A1, A3, FUNCT_2:def 2; verum