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

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