let z be set ; :: thesis: for f being Function st z in f [*] & rng f c= dom f holds
ex n being Nat st z in iter (f,n)
let f be Function; :: thesis: ( z in f [*] & rng f c= dom f implies ex n being Nat st z in iter (f,n) )
set LH = f [*] ;
assume C19: z in f [*] ; :: thesis: ( not rng f c= dom f or ex n being Nat st z in iter (f,n) )
then consider x, y being set such that
C8: z = [x,y] by RELAT_1:def 1;
consider p being FinSequence such that
C0: ( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in f ) ) by C8, C19, FINSEQ_1:def 16;
assume C9: rng f c= dom f ; :: thesis: ex n being Nat st z in iter (f,n)
then Z2: ( field f = dom f & x in field f ) by C8, C19, FINSEQ_1:def 16, XBOOLE_1:12;
consider m being Nat such that
C1: m + 1 = len p by C0, NAT_1:6;
take m ; :: thesis: z in iter (f,m)
for i being Nat st i >= 1 & i < len p holds
( p . i in dom f & p . (i + 1) = f . (p . i) )

proof

let i be Nat; :: thesis: ( i >= 1 & i < len p implies ( p . i in dom f & p . (i + 1) = f . (p . i) ) )
assume ( i >= 1 & i < len p ) ; :: thesis: ( p . i in dom f & p . (i + 1) = f . (p . i) )
then D0: [(p . i),(p . (i + 1))] in f by C0;
hence p . i in dom f by RELAT_1:def 4; :: thesis: p . (i + 1) = f . (p . i)
hence p . (i + 1) = f . (p . i) by D0, FUNCT_1:def 2; :: thesis: verum

end;

then C2: ( m + 1 >= 1 & p . 1 = x & p . (m + 1) = y & ( for i being Nat st i >= 1 & i < m + 1 holds
p . (i + 1) = f . (p . i) ) ) by C0, C1;
( x in dom (iter (f,m)) & p . (m + 1) = (iter (f,m)) . x ) by Z2, C9, C2, Lm36, FUNCT_7:74;
hence z in iter (f,m) by C8, C0, C1, FUNCT_1:1; :: thesis: verum