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 ) ) )

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 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 ;
A4: for i, j being Element of I st i <> j holds
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)}
proof
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 ;
then A7: 1_ G in F . i by GROUP_2:46;
A8: F . j is Subgroup of G by ;
then 1_ G in F . j by GROUP_2:46;
then 1_ G in ([#] (F . j)) /\ ([#] (F . i)) by ;
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
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 ;
reconsider gj = x as Element of (F . j) by A10;
gi in G by ;
then reconsider ggi = gi as Element of G ;
gj in G by ;
then reconsider ggj = gj as Element of G ;
x = 1_ G
proof
assume A11: x <> 1_ G ; :: thesis: contradiction
set xi = (1_ ()) +* (i,gi);
set xj = (1_ ()) +* (j,gj);
A12: (1_ ()) +* (i,gi) in sum F by ;
then reconsider xi = (1_ ()) +* (i,gi) as finite-support Function of I,G by ;
A13: (1_ ()) +* (j,gj) in sum F by ;
then reconsider xj = (1_ ()) +* (j,gj) as finite-support Function of I,G by ;
A14: 1_ () = I --> (1_ G) by ;
then Product xi = ggj by GROUP_19:21
.= Product xj by ;
then A15: xi = xj by ;
A16: dom (1_ ()) = I by GROUP_19:3;
xj . i = (1_ ()) . i by
.= 1_ (F . i) by GROUP_7:6
.= 1_ G by ;
hence contradiction by A11, A15, A16, FUNCT_7:31; :: thesis: verum
end;
hence x in {(1_ G)} by TARSKI:def 1; :: thesis: verum
end;
then ([#] (F . i)) /\ ([#] (F . j)) c= {(1_ G)} ;
hence ([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} by ; :: thesis: verum
end;
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
([#] (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 ; :: thesis: verum
end;
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 ) ) ; :: 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 ; :: thesis: verum