let z be set ; 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; ( z in f [*] & rng f c= dom f implies ex n being Nat st z in iter (f,n) )
set LH = f [*] ;
assume A1:
z in f [*]
; ( not rng f c= dom f or ex n being Nat st z in iter (f,n) )
then consider x, y being object such that
A2:
z = [x,y]
by RELAT_1:def 1;
consider p being FinSequence such that
A3:
( 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 A2, A1, FINSEQ_1:def 16;
assume A4:
rng f c= dom f
; ex n being Nat st z in iter (f,n)
then A5:
( field f = dom f & x in field f )
by A2, A1, FINSEQ_1:def 16, XBOOLE_1:12;
consider m being Nat such that
A6:
m + 1 = len p
by A3, NAT_1:6;
take
m
; 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) )
then A8:
( 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 A3, A6;
( x in dom (iter (f,m)) & p . (m + 1) = (iter (f,m)) . x )
by A5, A4, A8, Lm35, FUNCT_7:74;
hence
z in iter (f,m)
by A2, A3, A6, FUNCT_1:1; verum