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 is Subgroup of dprod F