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 A1: ( rng f c= dom f & a in dom f & g * f = g & a in A ) ; :: thesis: (A,g iter f) . a = (A,g iter f) . (f . a)
then A2: f . a in rng f by FUNCT_1:def 5;
then A3: f orbit (f . a) c= f orbit a by A1, Th9;

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

suppose A4: 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 A3, XBOOLE_1:1;
then (A,g iter f) . (f . a) = g . (f . a) by A1, A2, Def7
.= g . a by A1, FUNCT_1:23 ;
hence (A,g iter f) . a = (A,g iter f) . (f . a) by A1, A4, 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
A5: ( (A,g iter f) . a = (iter f,n) . a & (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) ) by A1, 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 A1, A5, FUNCT_1:35;
then n > 0 ;
then n >= 0 + 1 by NAT_1:13;
then consider i being Nat such that
A6: n = 1 + i by NAT_1:10;
iter f,n = (iter f,i) * f by A6, FUNCT_7:71;
then A7: (iter f,n) . a = (iter f,i) . (f . a) by A1, 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 j + 1 < n by A6, XREAL_1:10;
then ( iter f,(j + 1) = (iter f,j) * f & (iter f,(j + 1)) . a in A ) by A5, FUNCT_7:71;
hence (iter f,j) . (f . a) in A by A1, FUNCT_1:23; :: thesis: verum

end;

hence (A,g iter f) . a = (A,g iter f) . (f . a) by A1, A2, A5, A7, Def7; :: thesis: verum

end;

end;