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

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