set G = product F;
let x, y, z be Element of (product F); :: according to GROUP_1:def 3 :: 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;
A1: dom (Carrier F) = I by PARTFUN1:def 2;
then A2: dom t = I by CARD_3:9;

A3: now :: thesis: for i being object st i in I holds
s . i = t . i

let i be object ; :: thesis: ( i in I implies s . i = t . i )
assume A4: i in I ; :: thesis: s . i = t . i
then consider XY being non empty multMagma , hxy being Function such that
A5: XY = F . i and
A6: hxy = the multF of (product F) . (x,y) and
A7: hxy . i = the multF of XY . ((x1 . i),(y1 . i)) by Def2;
A8: ex YZ being non empty multMagma ex hyz being Function st
( YZ = F . i & hyz = the multF of (product F) . (y,z) & hyz . i = the multF of YZ . ((y1 . i),(z1 . i)) ) by A4, Def2;
reconsider xi = x1 . i, yi = y1 . i as Element of XY by A4, A5, Lm1;
consider XYZ1 being non empty multMagma , hxyz1 being Function such that
A9: XYZ1 = F . i and
A10: hxyz1 = the multF of (product F) . (xy,z) and
A11: hxyz1 . i = the multF of XYZ1 . ((xy . i),(z1 . i)) by A4, Def2;
reconsider zi = z1 . i, xiyi = xi * yi as Element of XYZ1 by A4, A5, A9, Lm1;
reconsider xii = xi, yii = yi as Element of XYZ1 by A5, A9;
A12: XYZ1 is associative by A4, A9, Def7;
A13: ex XYZ2 being non empty multMagma ex hxyz2 being Function st
( XYZ2 = F . i & hxyz2 = the multF of (product F) . (x,yz) & hxyz2 . i = the multF of XYZ2 . ((x1 . i),(yz . i)) ) by A4, Def2;
thus s . i = xiyi * zi by A6, A7, A10, A11
.= xii * (yii * zi) by A5, A9, A12
.= t . i by A8, A9, A13 ; :: thesis: verum

end;

dom s = I by A1, CARD_3:9;
hence (x * y) * z = x * (y * z) by A2, A3; :: thesis: verum