theorem Th7: :: YELLOW19:7

for S being non empty 1-sorted
for N being net of S
for i being Element of N
for x being set holds
( x in rng the mapping of (N | i) iff ex j being Element of N st
( i <= j & x = N . j ) )