for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for G being Group
for M being internal DirectSumComponents of G,I
for N being Group-Family of I,J st ( for i being Element of I holds N . i is internal DirectSumComponents of M . i,J . i ) holds
Union N is internal DirectSumComponents of G, Union J