:: deftheorem Def8 defines DirectSumComponents GROUP_19:def 8 :
for I being non empty set
for G being Group
for b₃ being Group-Family of I holds
( b₃ is DirectSumComponents of G,I iff ex h being Homomorphism of (sum b₃),G st h is bijective );