theorem Th16: :: WAYBEL_9:16

for L being non empty 1-sorted
for N being non empty directed NetStr over L
for i, x being Element of N
for x1 being Element of (N | i) st x = x1 holds
N . x = (N | i) . x1