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 dsum2sum F is bijective
let J be non-empty disjoint_valued ManySortedSet of I; :: thesis: for F being Group-Family of I,J holds dsum2sum F is bijective
let F be Group-Family of I,J; :: thesis: dsum2sum F is bijective
A1: dsum2sum F is one-to-one by FUNCT_1:52;
rng (dsum2sum F) = [#] (sum (Union F)) by Th33;
then dsum2sum F is onto by FUNCT_2:def 3;
hence dsum2sum F is bijective by A1; :: thesis: verum