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

proof

for j being object st j in I holds
x . j = (sy * sz) . j

proof

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

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

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;

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;

end;

end;

hence x = sy * sz by A9, A10, FUNCT_1:2; :: thesis: verum

end;

A17: sy * sz = sz * sy

proof

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;

A20: Product x = (Product y) * (Product z) by A2, A5, A12, GROUP_19:53;
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