set G = product F;
let x, y be Element of (product F); :: according to GROUP_1:def 16 :: 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;
dom (Carrier F) = I
by PARTFUN1:def 4;
then A1:
( dom xy = I & dom yx = I )
by CARD_3:18;
now let i be
set ;
:: thesis: ( i in I implies xy . i = yx . i )assume A2:
i in I
;
:: thesis: xy . i = yx . ithen consider XY being non
empty multMagma ,
hxy being
Function such that A3:
(
XY = F . i &
hxy = the
multF of
(product F) . x,
y &
hxy . i = the
multF of
XY . (x1 . i),
(y1 . i) )
by Def2;
consider YX being non
empty multMagma ,
hyx being
Function such that A4:
(
YX = F . i &
hyx = the
multF of
(product F) . y,
x &
hyx . i = the
multF of
YX . (y1 . i),
(x1 . i) )
by A2, Def2;
reconsider xi =
x1 . i,
yi =
y1 . i as
Element of
XY by A2, A3, Lm1;
consider Fi being non
empty commutative multMagma such that A5:
Fi = F . i
by A2, Def5;
thus xy . i =
xi * yi
by A3
.=
yi * xi
by A3, A5, GROUP_1:def 16
.=
yx . i
by A3, A4
;
:: thesis: verum end;
hence
x * y = y * x
by A1, FUNCT_1:9; :: thesis: verum