theorem Th36: :: GROUP_21:34

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 = (prod2dprod F) | (sum (Union F))