:: deftheorem Def4 defines multMagma-Family GROUP_21:def 4 :
for I being non empty set
for J, b₃ being ManySortedSet of I holds
( b₃ is multMagma-Family of I,J iff for i being Element of I holds b₃ . i is multMagma-Family of J . i );