let I be non empty set ; :: thesis: for F being Group-like associative multMagma-Family of I
for i, j being Element of I
for x, y being Element of (product F) st i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds
x * y = y * x
let F be Group-like associative multMagma-Family of I; :: thesis: for i, j being Element of I
for x, y being Element of (product F) st i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds
x * y = y * x
let i, j be Element of I; :: thesis: for x, y being Element of (product F) st i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds
x * y = y * x
set G = product F;
let x, y be Element of (product F); :: thesis: ( i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) implies x * y = y * x )
assume AS0: ( i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) ) ; :: thesis: x * y = y * x
PP: ( the carrier of (ProjGroup (F,i)) = ProjSet (F,i) & the carrier of (ProjGroup (F,j)) = ProjSet (F,j) ) by defPrjGroup;
AS1: ( x in ProjSet (F,i) & y in ProjSet (F,j) ) by PP, AS0, STRUCT_0:def 5;
consider xx being Function, gx being Element of (F . i) such that
X0: ( xx = x & dom xx = I & xx . i = gx & ( for k being Element of I st k <> i holds
xx . k = 1_ (F . k) ) ) by AS1, LMP1;
consider yy being Function, gy being Element of (F . j) such that
Y0: ( yy = y & dom yy = I & yy . j = gy & ( for k being Element of I st k <> j holds
yy . k = 1_ (F . k) ) ) by AS1, LMP1;
W0: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
set xy = x * y;
set yx = y * x;
XY1: dom (x * y) = I by PARTFUN1:def 4, W0;
YX1: dom (y * x) = I by PARTFUN1:def 4, W0;
for k being set st k in dom (x * y) holds
(x * y) . k = (y * x) . k

proof

let k0 be set ; :: thesis: ( k0 in dom (x * y) implies (x * y) . k0 = (y * x) . k0 )
assume k0 in dom (x * y) ; :: thesis: (x * y) . k0 = (y * x) . k0
then reconsider k = k0 as Element of I by PARTFUN1:def 4, W0;

per cases ( ( k0 <> i & k0 <> j ) or k0 = i or k0 = j ) ;

suppose C1: ( k0 <> i & k0 <> j ) ; :: thesis: (x * y) . k0 = (y * x) . k0

then C11: xx . k = 1_ (F . k) by X0;
C12: yy . k = 1_ (F . k) by C1, Y0;
(x * y) . k = (1_ (F . k)) * (1_ (F . k)) by X0, Y0, C11, C12, GROUP_7:4
.= (y * x) . k by X0, Y0, C11, C12, GROUP_7:4 ;
hence (x * y) . k0 = (y * x) . k0 ; :: thesis: verum

end;

suppose C2: ( k0 = i or k0 = j ) ; :: thesis: (x * y) . k0 = (y * x) . k0

per cases ( k0 = i or k0 = j ) by C2;

suppose C21: k0 = i ; :: thesis: (x * y) . k0 = (y * x) . k0

then C12: yy . k = 1_ (F . k) by AS0, Y0;
reconsider gx = gx as Element of (F . k) by C21;
(x * y) . k = gx * (1_ (F . k)) by X0, Y0, C12, C21, GROUP_7:4
.= gx by GROUP_1:def 5
.= (1_ (F . k)) * gx by GROUP_1:def 5
.= (y * x) . k by X0, Y0, C12, C21, GROUP_7:4 ;
hence (x * y) . k0 = (y * x) . k0 ; :: thesis: verum

end;

suppose C22: k0 = j ; :: thesis: (x * y) . k0 = (y * x) . k0

then C12: xx . k = 1_ (F . k) by AS0, X0;
reconsider gy = gy as Element of (F . k) by C22;
(x * y) . k = (1_ (F . k)) * gy by X0, Y0, C12, C22, GROUP_7:4
.= gy by GROUP_1:def 5
.= gy * (1_ (F . k)) by GROUP_1:def 5
.= (y * x) . k by X0, Y0, C12, C22, GROUP_7:4 ;
hence (x * y) . k0 = (y * x) . k0 ; :: thesis: verum

end;

end;

end;

end;

end;

hence x * y = y * x by XY1, YX1, FUNCT_1:9; :: thesis: verum