theorem :: YELLOW19:6

for S being non empty 1-sorted
for N being non empty NetStr over S
for i being Element of N holds rng the mapping of (N | i) is Subset of S,N by Def2;