set G = product F;
let x, y be Element of (product F); :: according to GROUP_1:def 12 :: thesis: x * y = y * x
reconsider x1 = x, y1 = y, xy = the multF of (product F) . (x,y), yx = the multF of (product F) . (y,x) as Element of product (Carrier F) by Def2;
A1: dom (Carrier F) = I by PARTFUN1:def 2;
then A2: dom yx = I by CARD_3:9;

A3: now :: thesis: for i being object st i in I holds
xy . i = yx . i

let i be object ; :: thesis: ( i in I implies xy . i = yx . i )
assume A4: i in I ; :: thesis: xy . i = yx . 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;
reconsider xi = x1 . i, yi = y1 . i as Element of XY by A4, A5, Lm1;
A8: ex YX being non empty multMagma ex hyx being Function st
( YX = F . i & hyx = the multF of (product F) . (y,x) & hyx . i = the multF of YX . ((y1 . i),(x1 . i)) ) by A4, Def2;
A9: ex Fi being non empty commutative multMagma st Fi = F . i by A4, Def5;
thus xy . i = xi * yi by A6, A7
.= yi * xi by A5, A9, GROUP_1:def 12
.= yx . i by A5, A8 ; :: thesis: verum

end;

dom xy = I by A1, CARD_3:9;
hence x * y = y * x by A2, A3; :: thesis: verum