let I be non empty set ; :: thesis: for G being Group
for F being component-commutative Subgroup-Family of I,G st ( for i being Element of I ex UFi being Subset of G st
( UFi = Union (() | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) holds
for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2

let G be Group; :: thesis: for F being component-commutative Subgroup-Family of I,G st ( for i being Element of I ex UFi being Subset of G st
( UFi = Union (() | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) holds
for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2

let F be component-commutative Subgroup-Family of I,G; :: thesis: ( ( for i being Element of I ex UFi being Subset of G st
( UFi = Union (() | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) implies for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2 )

A1: for i being object st i in I holds
F . i is Subgroup of G by Def1;
assume A2: for i being Element of I ex UFi being Subset of G st
( UFi = Union (() | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ; :: thesis: for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2

let x1, x2 be finite-support Function of I,G; :: thesis: ( x1 in sum F & x2 in sum F & Product x1 = Product x2 implies x1 = x2 )
assume that
A3: ( x1 in sum F & x2 in sum F ) and
A4: Product x1 = Product x2 ; :: thesis: x1 = x2
defpred S1[ Nat] means for x1, x2 being finite-support Function of I,G st card (support x1) = \$1 & x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2;
A5: S1[ 0 ]
proof
let x1, x2 be finite-support Function of I,G; :: thesis: ( card (support x1) = 0 & x1 in sum F & x2 in sum F & Product x1 = Product x2 implies x1 = x2 )
assume that
A6: card (support x1) = 0 and
A7: ( x1 in sum F & x2 in sum F ) and
A8: Product x1 = Product x2 ; :: thesis: x1 = x2
A9: support x1 = {} by A6;
A10: Product x2 = 1_ G by ;
x2 = 1_ ()
proof
assume x2 <> 1_ () ; :: thesis: contradiction
then not support x2 is empty by ;
then consider i being object such that
A11: i in support x2 by XBOOLE_0:def 1;
A12: ( x2 . i <> 1_ G & i in I ) by ;
reconsider i = i as Element of I by A11;
A13: F . i is Subgroup of G by Def1;
then 1_ (F . i) is Element of G by GROUP_2:42;
then reconsider y = x2 +* (i,(1_ (F . i))) as finite-support Function of I,G by GROUP_19:26;
x2 in product F by ;
then A14: Product x2 = () * (x2 . i) by Th8;
consider UFi being Subset of G such that
A15: UFi = Union (() | (I \ {i})) and
A16: ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} by A2;
A17: Product y in gr UFi by ;
x2 . i in F . i by ;
then A18: (x2 . i) " in F . i by ;
A19: Product y = (x2 . i) " by ;
then Product y in {(1_ G)} by ;
then Product y = 1_ G by TARSKI:def 1;
hence contradiction by A12, A19, GROUP_1:10; :: thesis: verum
end;
hence x1 = x2 by ; :: thesis: verum
end;
A20: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A21: S1[k] ; :: thesis: S1[k + 1]
let x1, x2 be finite-support Function of I,G; :: thesis: ( card (support x1) = k + 1 & x1 in sum F & x2 in sum F & Product x1 = Product x2 implies x1 = x2 )
assume that
A22: card (support x1) = k + 1 and
A23: ( x1 in sum F & x2 in sum F ) and
A24: Product x1 = Product x2 ; :: thesis: x1 = x2
not support x1 is empty by A22;
then consider i being object such that
A25: i in support x1 by XBOOLE_0:def 1;
reconsider i = i as Element of I by A25;
A26: F . i is Subgroup of G by Def1;
then A27: 1_ (F . i) is Element of G by GROUP_2:42;
reconsider y1 = x1 +* (i,(1_ (F . i))) as finite-support Function of I,G by ;
reconsider y2 = x2 +* (i,(1_ (F . i))) as finite-support Function of I,G by ;
consider UFi being Subset of G such that
A28: UFi = Union (() | (I \ {i})) and
A29: ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} by A2;
1_ (F . i) = 1_ G by ;
then A30: card (support y1) = (card (support x1)) - 1 by
.= k by A22 ;
A31: ( y1 in sum F & y2 in sum F ) by ;
A32: ( x1 in product F & x2 in product F ) by ;
A33: Product x1 = (Product y1) * (x1 . i) by ;
A34: ( Product y1 in gr UFi & Product y2 in gr UFi ) by ;
A35: ( x1 . i in F . i & x2 . i in F . i ) by ;
Product y1 = ((Product y2) * (x2 . i)) * ((x1 . i) ") by ;
then Product y1 = (Product y2) * ((x2 . i) * ((x1 . i) ")) by GROUP_1:def 3;
then A36: ((Product y2) ") * (Product y1) = (x2 . i) * ((x1 . i) ") by GROUP_1:13;
(Product y2) " in gr UFi by ;
then A37: ((Product y2) ") * (Product y1) in gr UFi by ;
(x1 . i) " in F . i by ;
then A38: (x2 . i) * ((x1 . i) ") in F . i by ;
((Product y2) ") * (Product y1) in {(1_ G)} by ;
then ((Product y2) ") * (Product y1) = 1_ G by TARSKI:def 1;
then (Product y1) " = (Product y2) " by GROUP_1:12;
then A39: y1 = y2 by ;
(x2 . i) * ((x1 . i) ") in {(1_ G)} by ;
then (x2 . i) * ((x1 . i) ") = 1_ G by TARSKI:def 1;
then (x1 . i) " = (x2 . i) " by GROUP_1:12;
then A40: x1 . i = x2 . i by GROUP_1:9;
x1 = y1 +* (i,(x1 . i)) by Th7;
hence x1 = x2 by ; :: thesis: verum
end;
A42: for k being Nat holds S1[k] from NAT_1:sch 2(A5, A20);
card (support x1) is Nat ;
hence x1 = x2 by A3, A4, A42; :: thesis: verum