theorem :: GROUP_21:44

for G being Group
for I1, I2 being non empty set
for F1 being internal DirectSumComponents of G,I1
for F2 being Subgroup-Family of I2,G st I1 misses I2 & F2 = I2 --> ((1). G) holds
F1 +* F2 is internal DirectSumComponents of G,I1 \/ I2