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 set such that
A3: y in f orbit a and
A4: y nin A by TARSKI:def 3;
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