set G = product F;
let x, y, z be Element of (product F); :: according to GROUP_1:def 4 :: thesis: (x * y) * z = x * (y * z)
reconsider x1 = x, y1 = y, z1 = z as Element of product (Carrier F) by Def2;
set xy = the multF of (product F) . x,y;
set yz = the multF of (product F) . y,z;
set s = the multF of (product F) . (the multF of (product F) . x,y),z;
set t = the multF of (product F) . x,(the multF of (product F) . y,z);
reconsider xy = the multF of (product F) . x,y, yz = the multF of (product F) . y,z, s = the multF of (product F) . (the multF of (product F) . x,y),z, t = the multF of (product F) . x,(the multF of (product F) . y,z) as Element of product (Carrier F) by Def2;
dom (Carrier F) = I
by PARTFUN1:def 4;
then A1:
( dom s = I & dom t = I )
by CARD_3:18;
now let i be
set ;
:: thesis: ( i in I implies s . i = t . i )assume A2:
i in I
;
:: thesis: s . i = t . ithen consider XY being non
empty multMagma ,
hxy being
Function such that A3:
(
XY = F . i &
hxy = the
multF of
(product F) . x,
y &
hxy . i = the
multF of
XY . (x1 . i),
(y1 . i) )
by Def2;
consider YZ being non
empty multMagma ,
hyz being
Function such that A4:
(
YZ = F . i &
hyz = the
multF of
(product F) . y,
z &
hyz . i = the
multF of
YZ . (y1 . i),
(z1 . i) )
by A2, Def2;
consider XYZ1 being non
empty multMagma ,
hxyz1 being
Function such that A5:
(
XYZ1 = F . i &
hxyz1 = the
multF of
(product F) . xy,
z &
hxyz1 . i = the
multF of
XYZ1 . (xy . i),
(z1 . i) )
by A2, Def2;
consider XYZ2 being non
empty multMagma ,
hxyz2 being
Function such that A6:
(
XYZ2 = F . i &
hxyz2 = the
multF of
(product F) . x,
yz &
hxyz2 . i = the
multF of
XYZ2 . (x1 . i),
(yz . i) )
by A2, Def2;
reconsider xi =
x1 . i,
yi =
y1 . i as
Element of
XY by A2, A3, Lm1;
reconsider zi =
z1 . i,
xiyi =
xi * yi as
Element of
XYZ1 by A2, A3, A5, Lm1;
reconsider xii =
xi,
yii =
yi as
Element of
XYZ1 by A3, A5;
A7:
XYZ1 is
associative
by A2, A5, Def7;
thus s . i =
xiyi * zi
by A3, A5
.=
xii * (yii * zi)
by A3, A5, A7, GROUP_1:def 4
.=
t . i
by A4, A5, A6
;
:: thesis: verum end;
hence
(x * y) * z = x * (y * z)
by A1, FUNCT_1:9; :: thesis: verum