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)):]