let G1, G2 be multMagma-Family of I; :: thesis: ( ( for i being Element of I holds G1 . i = product (F . i) ) & ( for i being Element of I holds G2 . i = product (F . i) ) implies G1 = G2 )
assume that
A4: for i being Element of I holds G1 . i = product (F . i) and
A5: for i being Element of I holds G2 . i = product (F . i) ; :: thesis: G1 = G2
A6: dom G1 = I by PARTFUN1:def 2;
for i being object st i in dom G1 holds
G1 . i = G2 . i

proof

let i be object ; :: thesis: ( i in dom G1 implies G1 . i = G2 . i )
assume i in dom G1 ; :: thesis: G1 . i = G2 . i
then reconsider i0 = i as Element of I ;
thus G1 . i = product (F . i0) by A4
.= G2 . i by A5 ; :: thesis: verum

end;

hence G1 = G2 by A6, PARTFUN1:def 2; :: thesis: verum