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 & y nin A ) by TARSKI:def 3;
consider n1 being Element of NAT such that
A4: ( y = (iter f,n1) . a & a in dom (iter f,n1) ) by A3;
defpred S₁[ Nat] means (iter f,$1) . a nin A;
A5: ex n being Nat st S₁[n] by A3, A4;
consider n being Nat such that
A6: S₁[n] and
A7: for m being Nat st S₁[m] holds
n <= m from NAT_1:sch 5(A5);
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 A7;
hence (A,g iter f) . a = (iter f,n) . a by A1, A2, A6, 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 A6, A7; :: thesis: verum