theorem Th1: :: BHSP_6:1

for X being RealUnitarySpace st the addF of X is commutative & the addF of X is associative & the addF of X is having_a_unity holds
for Y being finite Subset of X
for I being Function of the carrier of X, the carrier of X st Y c= dom I & ( for x being set st x in dom I holds
I . x = x ) holds
setsum Y = setopfunc (Y, the carrier of X, the carrier of X,I, the addF of X)