let f, g be Function; 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 ; ( 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
; ((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
;
((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;
verum end; suppose
not
f orbit a c= A
;
((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 for j being Nat st j < i holds
(iter (f,j)) . (f . a) in Alet j be
Nat;
( j < i implies (iter (f,j)) . (f . a) in A )assume
j < i
;
(iter (f,j)) . (f . a) in Athen 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;
verum end; hence
((A,g) iter f) . a = ((A,g) iter f) . (f . a)
by A1, A5, A8, A9, A12, Def7;
verum end;