:: deftheorem Def9 defines internal GROUP_19:def 9 :
for I being non empty set
for G being Group
for F being DirectSumComponents of G,I holds
( F is internal iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ex h being Homomorphism of (sum F),G st
( h is bijective & ( for x being finite-support Function of I,G st x in sum F holds
h . x = Product x ) ) ) );