let I be non empty set ; :: thesis: for J being non-empty ManySortedSet of I
for F being Group-Family of I,J holds dsum F is Subgroup of dprod F
let J be non-empty ManySortedSet of I; :: thesis: for F being Group-Family of I,J holds dsum F is Subgroup of dprod F
let F be Group-Family of I,J; :: thesis: dsum F is Subgroup of dprod F
for i being Element of I holds (sum_bundle F) . i is Subgroup of (prod_bundle F) . i

proof

let i be Element of I; :: thesis: (sum_bundle F) . i is Subgroup of (prod_bundle F) . i
(sum_bundle F) . i = sum (F . i) by Def7;
hence (sum_bundle F) . i is Subgroup of (prod_bundle F) . i by Def6; :: thesis: verum

end;

then product (sum_bundle F) is Subgroup of product (prod_bundle F) by Th20;
hence dsum F is Subgroup of dprod F by GROUP_2:56; :: thesis: verum