theorem :: GROUP_21:35

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 = (sum2dsum F) " by FUNCT_1:43;