:: deftheorem defines sum_byfunc BHSP_6:def 7 :

for X being RealUnitarySpace

for Y being Subset of X

for L being Functional of X st Y is_summable_set_by L holds

for b_{4} being Real holds

( b_{4} = sum_byfunc (Y,L) 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_{4} - (setopfunc (Y1, the carrier of X,REAL,L,addreal))).| < e ) ) );

for X being RealUnitarySpace

for Y being Subset of X

for L being Functional of X st Y is_summable_set_by L 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