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, z being Function st z in dprod F & x = (dprod2prod F) . z holds
( (supp_restr (x,F)) | (support (z,(sum_bundle F))) is non-empty disjoint_valued ManySortedSet of support (z,(sum_bundle F)) & support (x,(Union F)) = Union ((supp_restr (x,F)) | (support (z,(sum_bundle F)))) )