theorem Th26: :: YELLOW_6:26

for T being non empty 1-sorted
for N being net of T
for J being net_set of the carrier of N,T holds the carrier of (Iterated J) = [: the carrier of N,(product (Carrier J)):]