theorem :: GROUP_20:17

for I being non empty set
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 ) ) )