:: deftheorem defines sum BHSP_6:def 3 :

for X being RealUnitarySpace

for Y being Subset of X st Y is summable_set holds

for b_{3} being Point of X holds

( b_{3} = sum Y iff for e being Real st e > 0 holds

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

||.(b_{3} - (setsum Y1)).|| < e ) ) );

for X being RealUnitarySpace

for Y being Subset of X st Y is summable_set holds

for b

( b

ex Y0 being finite Subset of X st

( not Y0 is empty & Y0 c= Y & ( for Y1 being finite Subset of X st Y0 c= Y1 & Y1 c= Y holds

||.(b