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 () 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 () 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 () 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 (); :: thesis: ( i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) implies x * y = y * x )
assume A1: ( i <> j & x in ProjGroup (F,i) & y in ProjGroup (F,j) ) ; :: thesis: x * y = y * x
A2: ( the carrier of (ProjGroup (F,i)) = ProjSet (F,i) & the carrier of (ProjGroup (F,j)) = ProjSet (F,j) ) by Def2;
A3: ( x in ProjSet (F,i) & y in ProjSet (F,j) ) by ;
consider xx being Function, gx being Element of (F . i) such that
A4: ( xx = x & dom xx = I & xx . i = gx & ( for k being Element of I st k <> i holds
xx . k = 1_ (F . k) ) ) by ;
consider yy being Function, gy being Element of (F . j) such that
A5: ( yy = y & dom yy = I & yy . j = gy & ( for k being Element of I st k <> j holds
yy . k = 1_ (F . k) ) ) by ;
A6: the carrier of () = product () by GROUP_7:def 2;
set xy = x * y;
set yx = y * x;
A7: dom (x * y) = I by ;
A8: dom (y * x) = I by ;
for k being object st k in dom (x * y) holds
(x * y) . k = (y * x) . k
proof
let k0 be object ; :: 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 ;
per cases ( ( k0 <> i & k0 <> j ) or k0 = i or k0 = j ) ;
suppose A9: ( k0 <> i & k0 <> j ) ; :: thesis: (x * y) . k0 = (y * x) . k0
then A10: xx . k = 1_ (F . k) by A4;
A11: yy . k = 1_ (F . k) by A9, A5;
(x * y) . k = (1_ (F . k)) * (1_ (F . k)) by
.= (y * x) . k by ;
hence (x * y) . k0 = (y * x) . k0 ; :: thesis: verum
end;
suppose A12: ( k0 = i or k0 = j ) ; :: thesis: (x * y) . k0 = (y * x) . k0
per cases ( k0 = i or k0 = j ) by A12;
suppose A13: k0 = i ; :: thesis: (x * y) . k0 = (y * x) . k0
then A14: yy . k = 1_ (F . k) by A1, A5;
reconsider gx = gx as Element of (F . k) by A13;
(x * y) . k = gx * (1_ (F . k)) by
.= gx by GROUP_1:def 4
.= (1_ (F . k)) * gx by GROUP_1:def 4
.= (y * x) . k by ;
hence (x * y) . k0 = (y * x) . k0 ; :: thesis: verum
end;
suppose A15: k0 = j ; :: thesis: (x * y) . k0 = (y * x) . k0
then A16: xx . k = 1_ (F . k) by A1, A4;
reconsider gy = gy as Element of (F . k) by A15;
(x * y) . k = (1_ (F . k)) * gy by
.= gy by GROUP_1:def 4
.= gy * (1_ (F . k)) by GROUP_1:def 4
.= (y * x) . k by ;
hence (x * y) . k0 = (y * x) . k0 ; :: thesis: verum
end;
end;
end;
end;
end;
hence x * y = y * x by ; :: thesis: verum