:: 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₃ being Element of X holds
( b₃ = setsum Y iff ex p being FinSequence of the carrier of X st
( p is one-to-one & rng p = Y & b₃ = the addF of X "**" p ) );