deffunc H₁( object ) -> multMagma = product (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 = product (F . i)

proof

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

end;

for a being set st a in rng f holds
a is non empty multMagma

proof

let a be set ; :: thesis: ( a in rng f implies a is non empty multMagma )
assume a in rng f ; :: thesis: a is non empty multMagma
then consider i being object such that
A3: ( i in dom f & a = f . i ) by FUNCT_1:def 3;
reconsider i = i as Element of I by A3;
f . i = product (F . i) by A2;
hence a is non empty multMagma by A3; :: thesis: verum

end;

then reconsider f = f as multMagma-Family of I by GROUP_7:def 1;
take f ; :: thesis: for i being Element of I holds f . i = product (F . i)
thus for i being Element of I holds f . i = product (F . i) by A2; :: thesis: verum