let I be non empty set ; :: thesis: for G being commutative Group

for F being Group-Family of I holds

( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 commutative Group; :: thesis: for F being Group-Family of I holds

( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 Group-Family of I; :: thesis: ( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 ) ) )

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 ) ) ; :: thesis: F is internal DirectSumComponents of G,I

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 ;

hence F is internal DirectSumComponents of G,I by A17, GROUP_19:54; :: thesis: verum

for F being Group-Family of I holds

( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 commutative Group; :: thesis: for F being Group-Family of I holds

( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 Group-Family of I; :: thesis: ( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 ) ) )

hereby :: thesis: ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 ) implies F is internal DirectSumComponents of G,I )

assume A17:
( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 ) implies F is internal DirectSumComponents of G,I )

assume A1:
F is internal DirectSumComponents of G,I
; :: thesis: ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 ) )

then A2: ( ( for i being Element of I holds F . i is Subgroup of G ) & ( 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 ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 ) ) by GROUP_19:54;

A3: for i being object st i in I holds

F . i is Subgroup of G by A1, GROUP_19:54;

A4: for i, j being Element of I st i <> j holds

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 ) ) by A1, A4, GROUP_19:54; :: thesis: verum

end;([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 ) )

then A2: ( ( for i being Element of I holds F . i is Subgroup of G ) & ( 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 ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 ) ) by GROUP_19:54;

A3: for i being object st i in I holds

F . i is Subgroup of G by A1, GROUP_19:54;

A4: for i, j being Element of I st i <> j holds

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}

proof

thus
( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds
let i, j be Element of I; :: thesis: ( i <> j implies ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} )

assume A5: i <> j ; :: thesis: ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}

A6: F . i is Subgroup of G by A1, GROUP_19:54;

then A7: 1_ G in F . i by GROUP_2:46;

A8: F . j is Subgroup of G by A1, GROUP_19:54;

then 1_ G in F . j by GROUP_2:46;

then 1_ G in ([#] (F . j)) /\ ([#] (F . i)) by A7, XBOOLE_0:def 4;

then A9: {(1_ G)} c= ([#] (F . i)) /\ ([#] (F . j)) by ZFMISC_1:31;

for x being object st x in ([#] (F . i)) /\ ([#] (F . j)) holds

x in {(1_ G)}

hence ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} by A9, XBOOLE_0:def 10; :: thesis: verum

end;assume A5: i <> j ; :: thesis: ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}

A6: F . i is Subgroup of G by A1, GROUP_19:54;

then A7: 1_ G in F . i by GROUP_2:46;

A8: F . j is Subgroup of G by A1, GROUP_19:54;

then 1_ G in F . j by GROUP_2:46;

then 1_ G in ([#] (F . j)) /\ ([#] (F . i)) by A7, XBOOLE_0:def 4;

then A9: {(1_ G)} c= ([#] (F . i)) /\ ([#] (F . j)) by ZFMISC_1:31;

for x being object st x in ([#] (F . i)) /\ ([#] (F . j)) holds

x in {(1_ G)}

proof

then
([#] (F . i)) /\ ([#] (F . j)) c= {(1_ G)}
;
let x be object ; :: thesis: ( x in ([#] (F . i)) /\ ([#] (F . j)) implies x in {(1_ G)} )

assume A10: x in ([#] (F . i)) /\ ([#] (F . j)) ; :: thesis: x in {(1_ G)}

reconsider gi = x as Element of (F . i) by A10, XBOOLE_0:def 4;

reconsider gj = x as Element of (F . j) by A10;

gi in G by A6, GROUP_2:41;

then reconsider ggi = gi as Element of G ;

gj in G by A8, GROUP_2:41;

then reconsider ggj = gj as Element of G ;

x = 1_ G

end;assume A10: x in ([#] (F . i)) /\ ([#] (F . j)) ; :: thesis: x in {(1_ G)}

reconsider gi = x as Element of (F . i) by A10, XBOOLE_0:def 4;

reconsider gj = x as Element of (F . j) by A10;

gi in G by A6, GROUP_2:41;

then reconsider ggi = gi as Element of G ;

gj in G by A8, GROUP_2:41;

then reconsider ggj = gj as Element of G ;

x = 1_ G

proof

hence
x in {(1_ G)}
by TARSKI:def 1; :: thesis: verum
assume A11:
x <> 1_ G
; :: thesis: contradiction

set xi = (1_ (product F)) +* (i,gi);

set xj = (1_ (product F)) +* (j,gj);

A12: (1_ (product F)) +* (i,gi) in sum F by GROUP_19:25, GROUP_2:46;

then reconsider xi = (1_ (product F)) +* (i,gi) as finite-support Function of I,G by A3, GROUP_19:10;

A13: (1_ (product F)) +* (j,gj) in sum F by GROUP_19:25, GROUP_2:46;

then reconsider xj = (1_ (product F)) +* (j,gj) as finite-support Function of I,G by A3, GROUP_19:10;

A14: 1_ (product F) = I --> (1_ G) by A2, GROUP_19:13;

then Product xi = ggj by GROUP_19:21

.= Product xj by A14, GROUP_19:21 ;

then A15: xi = xj by A1, A12, A13, GROUP_19:54;

A16: dom (1_ (product F)) = I by GROUP_19:3;

xj . i = (1_ (product F)) . i by A5, FUNCT_7:32

.= 1_ (F . i) by GROUP_7:6

.= 1_ G by A6, GROUP_2:44 ;

hence contradiction by A11, A15, A16, FUNCT_7:31; :: thesis: verum

end;set xi = (1_ (product F)) +* (i,gi);

set xj = (1_ (product F)) +* (j,gj);

A12: (1_ (product F)) +* (i,gi) in sum F by GROUP_19:25, GROUP_2:46;

then reconsider xi = (1_ (product F)) +* (i,gi) as finite-support Function of I,G by A3, GROUP_19:10;

A13: (1_ (product F)) +* (j,gj) in sum F by GROUP_19:25, GROUP_2:46;

then reconsider xj = (1_ (product F)) +* (j,gj) as finite-support Function of I,G by A3, GROUP_19:10;

A14: 1_ (product F) = I --> (1_ G) by A2, GROUP_19:13;

then Product xi = ggj by GROUP_19:21

.= Product xj by A14, GROUP_19:21 ;

then A15: xi = xj by A1, A12, A13, GROUP_19:54;

A16: dom (1_ (product F)) = I by GROUP_19:3;

xj . i = (1_ (product F)) . i by A5, FUNCT_7:32

.= 1_ (F . i) by GROUP_7:6

.= 1_ G by A6, GROUP_2:44 ;

hence contradiction by A11, A15, A16, FUNCT_7:31; :: thesis: verum

hence ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} by A9, XBOOLE_0:def 10; :: thesis: verum

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 ) ) by A1, A4, GROUP_19:54; :: thesis: verum

([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st

( x in sum F & y = Product x ) ) & ( 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 ) ) ; :: thesis: F is internal DirectSumComponents of G,I

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 ;

hence F is internal DirectSumComponents of G,I by A17, GROUP_19:54; :: thesis: verum