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 ((Carrier F) | (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 ((Carrier F) | (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 ((Carrier F) | (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 ((Carrier F) | (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 S_{1}[ 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: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A5, A20);

card (support x1) is Nat ;

hence x1 = x2 by A3, A4, A42; :: thesis: verum

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 ((Carrier F) | (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 ((Carrier F) | (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 ((Carrier F) | (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 ((Carrier F) | (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 S

x1 = x2;

A5: S

proof

A20:
for k being Nat st S
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 A8, A9, GROUP_19:15;

x2 = 1_ (product F)

end;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 A8, A9, GROUP_19:15;

x2 = 1_ (product F)

proof

hence
x1 = x2
by A1, A9, GROUP_19:14; :: thesis: verum
assume
x2 <> 1_ (product F)
; :: thesis: contradiction

then not support x2 is empty by A1, GROUP_19:14;

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 A11, GROUP_19:def 2;

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 A7, GROUP_2:41;

then A14: Product x2 = (Product y) * (x2 . i) by Th8;

consider UFi being Subset of G such that

A15: UFi = Union ((Carrier F) | (I \ {i})) and

A16: ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} by A2;

A17: Product y in gr UFi by A7, A15, GROUP_2:41, Th12;

x2 . i in F . i by A7, GROUP_19:5, GROUP_2:41;

then A18: (x2 . i) " in F . i by A13, GROUP_2:51;

A19: Product y = (x2 . i) " by A10, A14, GROUP_1:12;

then Product y in {(1_ G)} by A16, A17, A18, XBOOLE_0:def 4;

then Product y = 1_ G by TARSKI:def 1;

hence contradiction by A12, A19, GROUP_1:10; :: thesis: verum

end;then not support x2 is empty by A1, GROUP_19:14;

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 A11, GROUP_19:def 2;

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 A7, GROUP_2:41;

then A14: Product x2 = (Product y) * (x2 . i) by Th8;

consider UFi being Subset of G such that

A15: UFi = Union ((Carrier F) | (I \ {i})) and

A16: ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} by A2;

A17: Product y in gr UFi by A7, A15, GROUP_2:41, Th12;

x2 . i in F . i by A7, GROUP_19:5, GROUP_2:41;

then A18: (x2 . i) " in F . i by A13, GROUP_2:51;

A19: Product y = (x2 . i) " by A10, A14, GROUP_1:12;

then Product y in {(1_ G)} by A16, A17, A18, XBOOLE_0:def 4;

then Product y = 1_ G by TARSKI:def 1;

hence contradiction by A12, A19, GROUP_1:10; :: thesis: verum

S

proof

A42:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A21: S_{1}[k]
; :: thesis: S_{1}[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 A27, GROUP_19:26;

reconsider y2 = x2 +* (i,(1_ (F . i))) as finite-support Function of I,G by A27, GROUP_19:26;

consider UFi being Subset of G such that

A28: UFi = Union ((Carrier F) | (I \ {i})) and

A29: ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} by A2;

1_ (F . i) = 1_ G by A26, GROUP_2:44;

then A30: card (support y1) = (card (support x1)) - 1 by A25, GROUP_19:30

.= k by A22 ;

A31: ( y1 in sum F & y2 in sum F ) by A23, GROUP_19:25;

A32: ( x1 in product F & x2 in product F ) by A23, GROUP_2:41;

A33: Product x1 = (Product y1) * (x1 . i) by A32, Th8;

A34: ( Product y1 in gr UFi & Product y2 in gr UFi ) by A23, A28, GROUP_2:41, Th12;

A35: ( x1 . i in F . i & x2 . i in F . i ) by A23, GROUP_19:5, GROUP_2:41;

Product y1 = ((Product y2) * (x2 . i)) * ((x1 . i) ") by A24, A32, A33, GROUP_1:14, Th8;

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 A34, GROUP_2:51;

then A37: ((Product y2) ") * (Product y1) in gr UFi by A34, GROUP_2:50;

(x1 . i) " in F . i by A26, A35, GROUP_2:51;

then A38: (x2 . i) * ((x1 . i) ") in F . i by A26, A35, GROUP_2:50;

((Product y2) ") * (Product y1) in {(1_ G)} by A29, A36, A37, A38, XBOOLE_0:def 4;

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 A21, A30, A31, GROUP_1:9;

(x2 . i) * ((x1 . i) ") in {(1_ G)} by A29, A36, A37, A38, XBOOLE_0:def 4;

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 A39, A40, Th7; :: thesis: verum

end;assume A21: S

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 A27, GROUP_19:26;

reconsider y2 = x2 +* (i,(1_ (F . i))) as finite-support Function of I,G by A27, GROUP_19:26;

consider UFi being Subset of G such that

A28: UFi = Union ((Carrier F) | (I \ {i})) and

A29: ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} by A2;

1_ (F . i) = 1_ G by A26, GROUP_2:44;

then A30: card (support y1) = (card (support x1)) - 1 by A25, GROUP_19:30

.= k by A22 ;

A31: ( y1 in sum F & y2 in sum F ) by A23, GROUP_19:25;

A32: ( x1 in product F & x2 in product F ) by A23, GROUP_2:41;

A33: Product x1 = (Product y1) * (x1 . i) by A32, Th8;

A34: ( Product y1 in gr UFi & Product y2 in gr UFi ) by A23, A28, GROUP_2:41, Th12;

A35: ( x1 . i in F . i & x2 . i in F . i ) by A23, GROUP_19:5, GROUP_2:41;

Product y1 = ((Product y2) * (x2 . i)) * ((x1 . i) ") by A24, A32, A33, GROUP_1:14, Th8;

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 A34, GROUP_2:51;

then A37: ((Product y2) ") * (Product y1) in gr UFi by A34, GROUP_2:50;

(x1 . i) " in F . i by A26, A35, GROUP_2:51;

then A38: (x2 . i) * ((x1 . i) ") in F . i by A26, A35, GROUP_2:50;

((Product y2) ") * (Product y1) in {(1_ G)} by A29, A36, A37, A38, XBOOLE_0:def 4;

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 A21, A30, A31, GROUP_1:9;

(x2 . i) * ((x1 . i) ") in {(1_ G)} by A29, A36, A37, A38, XBOOLE_0:def 4;

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 A39, A40, Th7; :: thesis: verum

card (support x1) is Nat ;

hence x1 = x2 by A3, A4, A42; :: thesis: verum