:: deftheorem defines sum2dsum GROUP_21:def 14 :
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J holds sum2dsum F = (dsum2sum F) " ;