theorem :: GROUP_19:54

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