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 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 A2, A1, STRUCT_0:def 5;
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 A3, Th2;
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 A3, Th2;
A6: the carrier of (product F) = product (Carrier F) by GROUP_7:def 2;
set xy = x * y;
set yx = y * x;
A7: dom (x * y) = I by A6, PARTFUN1:def 2;
A8: dom (y * x) = I by A6, PARTFUN1:def 2;
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 A6, PARTFUN1:def 2;
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 A4, A5, A10, A11, GROUP_7:1
.= (y * x) . k by A4, A5, A10, A11, GROUP_7:1 ;
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 A4, A5, A14, A13, GROUP_7:1
.= gx by GROUP_1:def 4
.= (1_ (F . k)) * gx by GROUP_1:def 4
.= (y * x) . k by A4, A5, A14, A13, GROUP_7:1 ;
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 A4, A5, A16, A15, GROUP_7:1
.= gy by GROUP_1:def 4
.= gy * (1_ (F . k)) by GROUP_1:def 4
.= (y * x) . k by A4, A5, A16, A15, GROUP_7:1 ;
hence (x * y) . k0 = (y * x) . k0 ; :: thesis: verum
end;
end;
end;
end;
end;
hence x * y = y * x by A7, A8, FUNCT_1:2; :: thesis: verum