let I be non empty set ; :: thesis:
let J be non-empty disjoint_valued ManySortedSet of I; :: thesis:
let F be Group-Family of I,J; :: thesis:
let x, y be Function; :: thesis:
assume A1: x in dsum F ; :: thesis:
then A2: x in dprod F by GROUP_2:40;
then reconsider y = (dprod2prod F) . x as Element of (product (Union F)) by FUNCT_2:5;
deffunc H₁( object ) -> Element of bool (J . (In ($1,I))) = support ((y | (J . (In ($1,I)))),(F . (In ($1,I))));
set sry = supp_restr (y,F);
reconsider sry1 = (supp_restr (y,F)) | (support (x,(sum_bundle F))) as non-empty disjoint_valued ManySortedSet of support (x,(sum_bundle F)) by A2, Th29;
for i being object st i in dom sry1 holds
sry1 . i is finite

let i be object ; :: thesis:
assume A3: i in dom sry1 ; :: thesis:
then i in support (x,(sum_bundle F)) ;
then reconsider i = i as Element of I ;
A4: y | (J . i) = x . i by A2, Def10;
x . i in (sum_bundle F) . i by A1, GROUP_2:40, GROUP_19:5;
then A5: x . i in sum (F . i) by Def7;
then x . i in product (F . i) by GROUP_2:40;
then reconsider zi = x . i as Element of (product (F . i)) ;
(supp_restr (y,F)) . i = support ((y | (J . i)),(F . i)) by Def12;
hence sry1 . i is finite by A3, A4, A5, FUNCT_1:49; :: thesis:

end;