let I be non empty set ; :: thesis: for G being Group
for F being internal DirectSumComponents of G,I holds F is Subgroup-Family of I,G
let G be Group; :: thesis: for F being internal DirectSumComponents of G,I holds F is Subgroup-Family of I,G
let F be internal DirectSumComponents of G,I; :: thesis: F is Subgroup-Family of I,G
for i being object st i in I holds
F . i is Subgroup of G by GROUP_19:def 9;
hence F is Subgroup-Family of I,G by GROUP_20:def 1; :: thesis: verum