theorem Th33: :: GROUP_21:33

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 rng ((dprod2prod F) | (dsum F)) = [#] (sum (Union F))