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 3;
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;
then ((A,g) iter f) . (f . a) = g . (f . a) by A1, A5, Def7
.= g . a by A2, A3, FUNCT_1:13 ;
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;
field f = dom f by A1, XBOOLE_1:12;
then iter (f,0) = id (dom f) by FUNCT_7:68;
then n <> 0 by A2, A4, A9, FUNCT_1:18;
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:69;
then A12: (iter (f,n)) . a = (iter (f,i)) . (f . a) by A2, FUNCT_1:13;

now :: thesis: for j being Nat st j < i holds
(iter (f,j)) . (f . a) in A

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:8;
A14: iter (f,(j + 1)) = (iter (f,j)) * f by FUNCT_7:69;
(iter (f,(j + 1))) . a in A by A10, A13;
hence (iter (f,j)) . (f . a) in A by A2, A14, FUNCT_1:13; :: 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;