let A, B be strict multMagma ; :: thesis:
assume that
A14: the carrier of A = product (Carrier F) and
A15: for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of A . f,g & h . i = the multF of Fi . (f . i),(g . i) ) and
A16: the carrier of B = product (Carrier F) and
A17: for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of B . f,g & h . i = the multF of Fi . (f . i),(g . i) ) ; :: thesis:
for x, y being set st x in the carrier of A & y in the carrier of A holds
the multF of A . x,y = the multF of B . x,y

let x, y be set ; :: thesis:
assume A18: ( x in the carrier of A & y in the carrier of A ) ; :: thesis:
set P = product (Carrier F);
reconsider x1 = x, y1 = y as Element of product (Carrier F) by A14, A18;
[x1,y1] in [:the carrier of A,the carrier of A:] by A18, ZFMISC_1:106;
then reconsider f = the multF of A . [x1,y1] as Element of product (Carrier F) by A14, FUNCT_2:7;
[x1,y1] in [:the carrier of B,the carrier of B:] by A16, ZFMISC_1:106;
then reconsider g = the multF of B . [x1,y1] as Element of product (Carrier F) by A16, FUNCT_2:7;
dom (Carrier F) = I by PBOOLE:def 3;
then A19: ( dom f = I & dom g = I ) by CARD_3:18;
for i being set st i in I holds
f . i = g . i

let i be set ; :: thesis:
assume A20: i in I ; :: thesis:
then consider Fi being non empty multMagma , h1 being Function such that
A21: ( Fi = F . i & h1 = the multF of A . x1,y1 & h1 . i = the multF of Fi . (x1 . i),(y1 . i) ) by A15;
ex Gi being non empty multMagma ex h2 being Function st
( Gi = F . i & h2 = the multF of B . x1,y1 & h2 . i = the multF of Gi . (x1 . i),(y1 . i) ) by A17, A20;
hence f . i = g . i by A21; :: thesis:

end;

hence the multF of A . x,y = the multF of B . x,y by A19, FUNCT_1:9; :: thesis:

end;

hence A = B by A14, A16, BINOP_1:1; :: thesis: