:: deftheorem defines prod2dprod GROUP_21:def 11 :
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 prod2dprod F = (dprod2prod F) " ;