:: deftheorem Def13 defines Iterated YELLOW_6:def 13 :
for T being non empty 1-sorted
for Y being net of T
for J being net_set of the carrier of Y,T
for b₄ being strict net of T holds
( b₄ = Iterated J iff ( RelStr(# the carrier of b₄, the InternalRel of b₄ #) = [:Y,(product J):] & ( for i being Element of Y
for f being Function st i in the carrier of Y & f in the carrier of (product J) holds
the mapping of b₄ . (i,f) = the mapping of (J . i) . (f . i) ) ) );