let f, g be Function; :: thesis: for a, A being set st rng f c= dom f & a in dom f & not f orbit a c= A holds
ex n being Nat st
( ((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 ) )
let a, A be set ; :: thesis: ( rng f c= dom f & a in dom f & not f orbit a c= A implies ex n being Nat st
( ((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 ) ) )
assume A1: rng f c= dom f ; :: thesis: ( not a in dom f or f orbit a c= A or ex n being Nat st
( ((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 ) ) )
assume A2: a in dom f ; :: thesis: ( f orbit a c= A or ex n being Nat st
( ((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 ) ) )
assume not f orbit a c= A ; :: thesis: ex n being Nat st
( ((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 ) )
then consider y being object such that
A3: y in f orbit a and
A4: y nin A ;
A5: ex n1 being Element of NAT st
( y = (iter (f,n1)) . a & a in dom (iter (f,n1)) ) by A3;
defpred S₁[ Nat] means (iter (f,$1)) . a nin A;
A6: ex n being Nat st S₁[n] by A4, A5;
consider n being Nat such that
A7: S₁[n] and
A8: for m being Nat st S₁[m] holds
n <= m from NAT_1:sch 5(A6);
take n ; :: thesis: ( ((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 ) )
for i being Nat st i < n holds
(iter (f,i)) . a in A by A8;
hence ((A,g) iter f) . a = (iter (f,n)) . a by A1, A2, A7, Def7; :: thesis: ( (iter (f,n)) . a nin A & ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) )
thus ( (iter (f,n)) . a nin A & ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) ) by A7, A8; :: thesis: verum