let A, B be strict multMagma ; :: thesis: ( the carrier of A = product (Carrier F) & ( 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)) ) ) & the carrier of B = product (Carrier F) & ( 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)) ) ) implies A = B )

assume that

A17: the carrier of A = product (Carrier F) and

A18: 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

A19: the carrier of B = product (Carrier F) and

A20: 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: A = B

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)

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)) ) ) & the carrier of B = product (Carrier F) & ( 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)) ) ) implies A = B )

assume that

A17: the carrier of A = product (Carrier F) and

A18: 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

A19: the carrier of B = product (Carrier F) and

A20: 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: A = B

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)

proof

hence
A = B
by A17, A19, BINOP_1:1; :: thesis: verum
set P = product (Carrier F);

let x, y be set ; :: thesis: ( x in the carrier of A & y in the carrier of A implies the multF of A . (x,y) = the multF of B . (x,y) )

assume that

A21: x in the carrier of A and

A22: y in the carrier of A ; :: thesis: the multF of A . (x,y) = the multF of B . (x,y)

reconsider x1 = x, y1 = y as Element of product (Carrier F) by A17, A21, A22;

[x1,y1] in [: the carrier of A, the carrier of A:] by A21, A22, ZFMISC_1:87;

then reconsider f = the multF of A . [x1,y1] as Element of product (Carrier F) by A17, FUNCT_2:5;

[x1,y1] in [: the carrier of B, the carrier of B:] by A19, ZFMISC_1:87;

then reconsider g = the multF of B . [x1,y1] as Element of product (Carrier F) by A19, FUNCT_2:5;

A23: dom (Carrier F) = I by PARTFUN1:def 2;

then A24: dom g = I by CARD_3:9;

A25: for i being object st i in I holds

f . i = g . i

hence the multF of A . (x,y) = the multF of B . (x,y) by A24, A25, FUNCT_1:2; :: thesis: verum

end;let x, y be set ; :: thesis: ( x in the carrier of A & y in the carrier of A implies the multF of A . (x,y) = the multF of B . (x,y) )

assume that

A21: x in the carrier of A and

A22: y in the carrier of A ; :: thesis: the multF of A . (x,y) = the multF of B . (x,y)

reconsider x1 = x, y1 = y as Element of product (Carrier F) by A17, A21, A22;

[x1,y1] in [: the carrier of A, the carrier of A:] by A21, A22, ZFMISC_1:87;

then reconsider f = the multF of A . [x1,y1] as Element of product (Carrier F) by A17, FUNCT_2:5;

[x1,y1] in [: the carrier of B, the carrier of B:] by A19, ZFMISC_1:87;

then reconsider g = the multF of B . [x1,y1] as Element of product (Carrier F) by A19, FUNCT_2:5;

A23: dom (Carrier F) = I by PARTFUN1:def 2;

then A24: dom g = I by CARD_3:9;

A25: for i being object st i in I holds

f . i = g . i

proof

dom f = I
by A23, CARD_3:9;
let i be object ; :: thesis: ( i in I implies f . i = g . i )

assume A26: i in I ; :: thesis: f . i = g . i

then A27: 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 A20;

ex Fi being non empty multMagma ex h1 being Function st

( Fi = F . i & h1 = the multF of A . (x1,y1) & h1 . i = the multF of Fi . ((x1 . i),(y1 . i)) ) by A18, A26;

hence f . i = g . i by A27; :: thesis: verum

end;assume A26: i in I ; :: thesis: f . i = g . i

then A27: 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 A20;

ex Fi being non empty multMagma ex h1 being Function st

( Fi = F . i & h1 = the multF of A . (x1,y1) & h1 . i = the multF of Fi . ((x1 . i),(y1 . i)) ) by A18, A26;

hence f . i = g . i by A27; :: thesis: verum

hence the multF of A . (x,y) = the multF of B . (x,y) by A24, A25, FUNCT_1:2; :: thesis: verum