theorem Th27: :: YELLOW_6:27

for T being non empty 1-sorted
for N being net of T
for J being net_set of the carrier of N,T
for i being Element of N
for f being Element of (product J)
for x being Element of (Iterated J) st x = [i,f] holds
(Iterated J) . x = the mapping of (J . i) . (f . i)