theorem Th7: :: WAYBEL28:7

for L being non empty 1-sorted
for N being non empty NetStr over L
for f being Function of N,N holds N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #)