let A, B be strict multMagma ; ( 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)) )
; 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
set P =
product (Carrier F);
let x,
y be
set ;
( 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
;
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
dom f = I
by A23, CARD_3:9;
hence
the
multF of
A . (
x,
y)
= the
multF of
B . (
x,
y)
by A24, A25, FUNCT_1:2;
verum
end;
hence
A = B
by A17, A19, BINOP_1:1; verum