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 A1: 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 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 ; :: thesis: 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 ; :: 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 A7: [(p . i),(p . (i + 1))] in f by A3;
hence p . i in dom f by XTUPLE_0:def 12; :: thesis: p . (i + 1) = f . (p . i)
hence p . (i + 1) = f . (p . i) by FUNCT_1:def 2, A7; :: thesis: verum
end;
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; :: thesis: verum