:: deftheorem Def1 defines setsum BHSP_6:def 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 b_{3} being Element of X holds

( b_{3} = setsum Y iff ex p being FinSequence of the carrier of X st

( p is one-to-one & rng p = Y & b_{3} = the addF of X "**" p ) );

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 b

( b

( p is one-to-one & rng p = Y & b