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