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;

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

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

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

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