for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for x, y being Function st x in dsum F & x in dsum F holds
(dprod2prod F) . x in sum (Union F)