for I2 being non empty set
for F2 being Group-Family of I2 st ( for i being Element of I2 holds card (F2 . i) = 1 ) holds
card the carrier of (sum F2) = 1