for I being non empty set
for F being Group-Family of I
for i being Element of I holds ProjGroup (F,i) is Subgroup of sum F