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