let f, g be Function; :: thesis: for a, A being set st rng f c= dom f & a in dom f & g * f = g & a in A holds
(A,g iter f) . a = (A,g iter f) . (f . a)
let a, A be set ; :: thesis: ( rng f c= dom f & a in dom f & g * f = g & a in A implies (A,g iter f) . a = (A,g iter f) . (f . a) )
assume that
A1: rng f c= dom f and
A2: a in dom f and
A3: g * f = g and
A4: a in A ; :: thesis: (A,g iter f) . a = (A,g iter f) . (f . a)
A5: f . a in rng f by A2, FUNCT_1:def 5;
A6: f orbit (f . a) c= f orbit a by A2, Th9;

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

suppose A7: f orbit a c= A ; :: thesis: (A,g iter f) . a = (A,g iter f) . (f . a)

then f orbit (f . a) c= A by A6, XBOOLE_1:1;
then (A,g iter f) . (f . a) = g . (f . a) by A1, A5, Def7
.= g . a by A2, A3, FUNCT_1:23 ;
hence (A,g iter f) . a = (A,g iter f) . (f . a) by A1, A2, A7, Def7; :: thesis: verum

end;

suppose not f orbit a c= A ; :: thesis: (A,g iter f) . a = (A,g iter f) . (f . a)

then consider n being Nat such that
A8: (A,g iter f) . a = (iter f,n) . a and
A9: (iter f,n) . a nin A and
A10: for i being Nat st i < n holds
(iter f,i) . a in A by A1, A2, Th10;
(dom f) \/ (rng f) = dom f by A1, XBOOLE_1:12;
then iter f,0 = id (dom f) by FUNCT_7:70;
then n <> 0 by A2, A4, A9, FUNCT_1:35;
then n >= 0 + 1 by NAT_1:13;
then consider i being Nat such that
A11: n = 1 + i by NAT_1:10;
iter f,n = (iter f,i) * f by A11, FUNCT_7:71;
then A12: (iter f,n) . a = (iter f,i) . (f . a) by A2, FUNCT_1:23;

now

let j be Nat; :: thesis: ( j < i implies (iter f,j) . (f . a) in A )
assume j < i ; :: thesis: (iter f,j) . (f . a) in A
then A13: j + 1 < n by A11, XREAL_1:10;
A14: iter f,(j + 1) = (iter f,j) * f by FUNCT_7:71;
(iter f,(j + 1)) . a in A by A10, A13;
hence (iter f,j) . (f . a) in A by A2, A14, FUNCT_1:23; :: thesis: verum

end;

hence (A,g iter f) . a = (A,g iter f) . (f . a) by A1, A5, A8, A9, A12, Def7; :: thesis: verum

end;

end;