:: deftheorem defines dsum GROUP_21:def 9 :
for I being non empty set
for J being non-empty ManySortedSet of I
for F being Group-Family of I,J holds dsum F = sum (sum_bundle F);