let I be non empty set ; 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; 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; ( ( 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)} )
; 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; ( 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
; 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;
( 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
;
x1 = x2
A9:
support x1 = {}
by A6;
A10:
Product x2 = 1_ G
by A8, A9, GROUP_19:15;
x2 = 1_ (product F)
proof
assume
x2 <> 1_ (product F)
;
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;
verum
end;
hence
x1 = x2
by A1, A9, GROUP_19:14;
verum
end;
A20:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A21:
S1[
k]
;
S1[k + 1]
let x1,
x2 be
finite-support Function of
I,
G;
( 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
;
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;
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; verum