theorem :: GROUP_19:29

for I being non empty set
for F being Group-Family of I
for i being Element of I
for a being Element of (sum F)
for b being Function st i in support (a,F) & b = a +* (i,(1_ (F . i))) holds
card (support (b,F)) = (card (support (a,F))) - 1