deffunc H₁( object ) -> Subgroup of product (F . (In ($1,I))) = sum (F . (In ($1,I)));
consider f being Function such that
A1: ( dom f = I & ( for i being Element of I holds f . i = H₁(i) ) ) from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;
A2: for i being Element of I holds f . i = sum (F . i)

proof

let i be Element of I; :: thesis: f . i = sum (F . i)
In (i,I) = i ;
hence f . i = sum (F . i) by A1; :: thesis: verum

end;

for i being object st i in I holds
f . i is Group

proof

let i be object ; :: thesis: ( i in I implies f . i is Group )
assume i in I ; :: thesis: f . i is Group
then reconsider i = i as Element of I ;
f . i = sum (F . i) by A2;
hence f . i is Group ; :: thesis: verum

end;

then f is Group-Family of I by A1, GROUP_19:2;
hence ex b₁ being Group-Family of I st
for i being Element of I holds b₁ . i = sum (F . i) by A2; :: thesis: verum