let I be non empty set ; :: thesis: for G being Group

for F being component-commutative Subgroup-Family of I,G

for x, y being finite-support Function of I,G

for i being Element of I st y = x +* (i,(1_ (F . i))) & x in product F holds

( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

let G be Group; :: thesis: for F being component-commutative Subgroup-Family of I,G

for x, y being finite-support Function of I,G

for i being Element of I st y = x +* (i,(1_ (F . i))) & x in product F holds

( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

let F be component-commutative Subgroup-Family of I,G; :: thesis: for x, y being finite-support Function of I,G

for i being Element of I st y = x +* (i,(1_ (F . i))) & x in product F holds

( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

let x, y be finite-support Function of I,G; :: thesis: for i being Element of I st y = x +* (i,(1_ (F . i))) & x in product F holds

( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

let i be Element of I; :: thesis: ( y = x +* (i,(1_ (F . i))) & x in product F implies ( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) ) )

A1: for i being object st i in I holds

F . i is Subgroup of G by Def1;

A2: for i, j being Element of I

for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds

gi * gj = gj * gi by Def2;

assume that

A3: y = x +* (i,(1_ (F . i))) and

A4: x in product F ; :: thesis: ( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

A5: for i being Element of I holds F . i is Subgroup of G by Def1;

reconsider px = x as Element of (product F) by A4;

A6: x . i in F . i by A4, GROUP_19:5;

y in product F by A3, A4, GROUP_19:24;

then reconsider py = y as Element of (product F) ;

support y = support (py,F) by A1, GROUP_19:9;

then py in sum F by GROUP_19:8;

then reconsider sy = py as Element of (sum F) ;

set z = (1_ (product F)) +* (i,(x . i));

A7: (1_ (product F)) +* (i,(x . i)) in sum F by A6, GROUP_19:25, GROUP_2:46;

then A8: (1_ (product F)) +* (i,(x . i)) in product F by GROUP_2:40;

reconsider sz = (1_ (product F)) +* (i,(x . i)) as Element of (sum F) by A7;

reconsider pz = (1_ (product F)) +* (i,(x . i)) as Element of (product F) by A8;

reconsider z = (1_ (product F)) +* (i,(x . i)) as finite-support Function of I,G by A1, A7, GROUP_19:10;

A9: dom x = I by A4, GROUP_19:3;

sy * sz is Element of (product F) by GROUP_2:42;

then A10: dom (sy * sz) = I by GROUP_19:3;

A11: dom (1_ (product F)) = I by GROUP_19:3;

A12: x = sy * sz

1_ (product F) = I --> (1_ G) by A5, GROUP_19:13;

then Product z = x . i by GROUP_19:21;

hence ( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) ) by A2, A5, A12, A17, A20, GROUP_19:53; :: thesis: verum

for F being component-commutative Subgroup-Family of I,G

for x, y being finite-support Function of I,G

for i being Element of I st y = x +* (i,(1_ (F . i))) & x in product F holds

( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

let G be Group; :: thesis: for F being component-commutative Subgroup-Family of I,G

for x, y being finite-support Function of I,G

for i being Element of I st y = x +* (i,(1_ (F . i))) & x in product F holds

( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

let F be component-commutative Subgroup-Family of I,G; :: thesis: for x, y being finite-support Function of I,G

for i being Element of I st y = x +* (i,(1_ (F . i))) & x in product F holds

( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

let x, y be finite-support Function of I,G; :: thesis: for i being Element of I st y = x +* (i,(1_ (F . i))) & x in product F holds

( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

let i be Element of I; :: thesis: ( y = x +* (i,(1_ (F . i))) & x in product F implies ( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) ) )

A1: for i being object st i in I holds

F . i is Subgroup of G by Def1;

A2: for i, j being Element of I

for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds

gi * gj = gj * gi by Def2;

assume that

A3: y = x +* (i,(1_ (F . i))) and

A4: x in product F ; :: thesis: ( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

A5: for i being Element of I holds F . i is Subgroup of G by Def1;

reconsider px = x as Element of (product F) by A4;

A6: x . i in F . i by A4, GROUP_19:5;

y in product F by A3, A4, GROUP_19:24;

then reconsider py = y as Element of (product F) ;

support y = support (py,F) by A1, GROUP_19:9;

then py in sum F by GROUP_19:8;

then reconsider sy = py as Element of (sum F) ;

set z = (1_ (product F)) +* (i,(x . i));

A7: (1_ (product F)) +* (i,(x . i)) in sum F by A6, GROUP_19:25, GROUP_2:46;

then A8: (1_ (product F)) +* (i,(x . i)) in product F by GROUP_2:40;

reconsider sz = (1_ (product F)) +* (i,(x . i)) as Element of (sum F) by A7;

reconsider pz = (1_ (product F)) +* (i,(x . i)) as Element of (product F) by A8;

reconsider z = (1_ (product F)) +* (i,(x . i)) as finite-support Function of I,G by A1, A7, GROUP_19:10;

A9: dom x = I by A4, GROUP_19:3;

sy * sz is Element of (product F) by GROUP_2:42;

then A10: dom (sy * sz) = I by GROUP_19:3;

A11: dom (1_ (product F)) = I by GROUP_19:3;

A12: x = sy * sz

proof

A17:
sy * sz = sz * sy
for j being object st j in I holds

x . j = (sy * sz) . j

end;x . j = (sy * sz) . j

proof

hence
x = sy * sz
by A9, A10, FUNCT_1:2; :: thesis: verum
let j be object ; :: thesis: ( j in I implies x . j = (sy * sz) . j )

assume j in I ; :: thesis: x . j = (sy * sz) . j

then reconsider j = j as Element of I ;

y . j in F . j by A3, A4, GROUP_19:5, GROUP_19:24;

then reconsider yj = y . j as Element of (F . j) ;

z . j in F . j by A7, GROUP_19:5, GROUP_2:40;

then reconsider zj = z . j as Element of (F . j) ;

end;assume j in I ; :: thesis: x . j = (sy * sz) . j

then reconsider j = j as Element of I ;

y . j in F . j by A3, A4, GROUP_19:5, GROUP_19:24;

then reconsider yj = y . j as Element of (F . j) ;

z . j in F . j by A7, GROUP_19:5, GROUP_2:40;

then reconsider zj = z . j as Element of (F . j) ;

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

end;

suppose A13:
j = i
; :: thesis: x . j = (sy * sz) . j

then A14:
y . j = 1_ (F . j)
by A3, A9, FUNCT_7:31;

z . j = x . j by A11, A13, FUNCT_7:31;

then yj * zj = x . j by A14, GROUP_1:def 4;

then px . j = (py * pz) . j by GROUP_7:1;

hence x . j = (sy * sz) . j by GROUP_2:43; :: thesis: verum

end;z . j = x . j by A11, A13, FUNCT_7:31;

then yj * zj = x . j by A14, GROUP_1:def 4;

then px . j = (py * pz) . j by GROUP_7:1;

hence x . j = (sy * sz) . j by GROUP_2:43; :: thesis: verum

suppose A15:
j <> i
; :: thesis: x . j = (sy * sz) . j

then A16:
y . j = x . j
by A3, FUNCT_7:32;

(1_ (product F)) . j = 1_ (F . j) by GROUP_7:6;

then z . j = 1_ (F . j) by A15, FUNCT_7:32;

then yj * zj = x . j by A16, GROUP_1:def 4;

then px . j = (py * pz) . j by GROUP_7:1;

hence x . j = (sy * sz) . j by GROUP_2:43; :: thesis: verum

end;(1_ (product F)) . j = 1_ (F . j) by GROUP_7:6;

then z . j = 1_ (F . j) by A15, FUNCT_7:32;

then yj * zj = x . j by A16, GROUP_1:def 4;

then px . j = (py * pz) . j by GROUP_7:1;

hence x . j = (sy * sz) . j by GROUP_2:43; :: thesis: verum

proof

A20:
Product x = (Product y) * (Product z)
by A2, A5, A12, GROUP_19:53;
A18:
support (py,F) = (support (px,F)) \ {i}
by A3, A9, GROUP_19:27;

A19: support (py,F) misses support (pz,F) by A6, A18, GROUP_19:17, XBOOLE_1:85;

thus sy * sz = py * pz by GROUP_2:43

.= pz * py by A19, GROUP_19:32

.= sz * sy by GROUP_2:43 ; :: thesis: verum

end;A19: support (py,F) misses support (pz,F) by A6, A18, GROUP_19:17, XBOOLE_1:85;

thus sy * sz = py * pz by GROUP_2:43

.= pz * py by A19, GROUP_19:32

.= sz * sy by GROUP_2:43 ; :: thesis: verum

1_ (product F) = I --> (1_ G) by A5, GROUP_19:13;

then Product z = x . i by GROUP_19:21;

hence ( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) ) by A2, A5, A12, A17, A20, GROUP_19:53; :: thesis: verum