theorem :: GROUP_19:30

for I being non empty set
for G being Group
for i being object
for a being finite-support Function of I,G
for b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds
card (support b) = (card (support a)) - 1