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)

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)