theorem Th26: :: WAYBEL11:26

for S being non empty 1-sorted
for e being Element of S
for x being Element of (Net-Str e) holds (Net-Str e) . x = e