theorem Th6: :: WAYBEL28:6

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