:: deftheorem Def6 defines prod_bundle GROUP_21:def 6 :
for I being non empty set
for J being ManySortedSet of I
for F being multMagma-Family of I,J
for b₄ being multMagma-Family of I holds
( b₄ = prod_bundle F iff for i being Element of I holds b₄ . i = product (F . i) );