:: deftheorem defines dsum2sum GROUP_21:def 13 :
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 dsum2sum F = (dprod2prod F) | (dsum F);