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 = () * (x . i) & () * (x . i) = (x . i) * () )

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 = () * (x . i) & () * (x . i) = (x . i) * () )

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 = () * (x . i) & () * (x . i) = (x . i) * () )

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 = () * (x . i) & () * (x . i) = (x . i) * () )

let i be Element of I; :: thesis: ( y = x +* (i,(1_ (F . i))) & x in product F implies ( Product x = () * (x . i) & () * (x . i) = (x . i) * () ) )
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 = () * (x . i) & () * (x . i) = (x . i) * () )
A5: for i being Element of I holds F . i is Subgroup of G by Def1;
reconsider px = x as Element of () by A4;
A6: x . i in F . i by ;
y in product F by ;
then reconsider py = y as Element of () ;
support y = support (py,F) by ;
then py in sum F by GROUP_19:8;
then reconsider sy = py as Element of (sum F) ;
set z = (1_ ()) +* (i,(x . i));
A7: (1_ ()) +* (i,(x . i)) in sum F by ;
then A8: (1_ ()) +* (i,(x . i)) in product F by GROUP_2:40;
reconsider sz = (1_ ()) +* (i,(x . i)) as Element of (sum F) by A7;
reconsider pz = (1_ ()) +* (i,(x . i)) as Element of () by A8;
reconsider z = (1_ ()) +* (i,(x . i)) as finite-support Function of I,G by ;
A9: dom x = I by ;
sy * sz is Element of () by GROUP_2:42;
then A10: dom (sy * sz) = I by GROUP_19:3;
A11: dom (1_ ()) = 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 ;
then reconsider yj = y . j as Element of (F . j) ;
z . j in F . j by ;
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 ;
z . j = x . j by ;
then yj * zj = x . j by ;
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 ;
(1_ ()) . j = 1_ (F . j) by GROUP_7:6;
then z . j = 1_ (F . j) by ;
then yj * zj = x . j by ;
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 ; :: thesis: verum
end;
A17: sy * sz = sz * sy
proof
A18: support (py,F) = (support (px,F)) \ {i} by ;
A19: support (py,F) misses support (pz,F) by ;
thus sy * sz = py * pz by GROUP_2:43
.= pz * py by
.= sz * sy by GROUP_2:43 ; :: thesis: verum
end;
A20: Product x = () * () by ;
1_ () = I --> (1_ G) by ;
then Product z = x . i by GROUP_19:21;
hence ( Product x = () * (x . i) & () * (x . i) = (x . i) * () ) by ; :: thesis: verum