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;

hence (x * y) * z = x * (y * z) by A2, A3; :: thesis: verum

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

dom s = I
by A1, CARD_3:9;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;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

hence (x * y) * z = x * (y * z) by A2, A3; :: thesis: verum