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

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

hence
x * y = y * x
by A7, A8, FUNCT_1:2; :: thesis: verum
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;

end;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 )
;

end;

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;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

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

end;

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

end;

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;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

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;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