for I being non empty set
for G being Group
for F being internal DirectSumComponents of G,I holds F is Subgroup-Family of I,G