let I be non empty set ; :: thesis: 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))
let J be non-empty disjoint_valued ManySortedSet of I; :: thesis: for F being Group-Family of I,J holds sum2dsum F = (prod2dprod F) | (sum (Union F))
let F be Group-Family of I,J; :: thesis: sum2dsum F = (prod2dprod F) | (sum (Union F))
dsum2sum F is bijective ;
then rng ((dprod2prod F) | (dsum F)) = [#] (sum (Union F)) by FUNCT_2:def 3;
hence sum2dsum F = (prod2dprod F) | (sum (Union F)) by Th35; :: thesis: verum