set G = product F;
let x, y be Element of (); :: according to GROUP_1:def 12 :: thesis: x * y = y * x
reconsider x1 = x, y1 = y, xy = the multF of () . (x,y), yx = the multF of () . (y,x) as Element of product () by Def2;
A1: dom () = 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 () . (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 () . (y,x) & hyx . i = the multF of YX . ((y1 . i),(x1 . i)) ) by ;
A9: ex Fi being non empty commutative multMagma st Fi = F . i by ;
thus xy . i = xi * yi by A6, A7
.= yi * xi by
.= yx . i by A5, A8 ; :: thesis: verum
end;
dom xy = I by ;
hence x * y = y * x by A2, A3; :: thesis: verum