set G = product F;
let x, y be Element of (product F); GROUP_1:def 12 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 for i being object st i in I holds
xy . i = yx . ilet i be
object ;
( i in I implies xy . i = yx . i )assume A4:
i in I
;
xy . i = yx . ithen 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
;
verum end;
dom xy = I
by A1, CARD_3:9;
hence
x * y = y * x
by A2, A3; verum