let T be non empty 1-sorted ; :: thesis: for N being non empty NetStr of T holds N is_eventually_in rng the mapping of N
let N be non empty NetStr of T; :: thesis: N is_eventually_in rng the mapping of N
consider i being Element of N;
take i ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of N holds
( not i <= b₁ or N . b₁ in rng the mapping of N )
let j be Element of N; :: thesis: ( not i <= j or N . j in rng the mapping of N )
assume i <= j ; :: thesis: N . j in rng the mapping of N
thus N . j in rng the mapping of N by FUNCT_2:6; :: thesis: verum