deffunc H1( 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 = H1(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 b1 being Group-Family of I st
for i being Element of I holds b1 . i = sum (F . i) by A2; :: thesis: verum