theorem :: BHSP_6:10

for X being RealHilbertSpace 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 Subset of X holds

( Y is summable_set 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 not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

||.(setsum Y1).|| < e ) ) )

for Y being Subset of X holds

( Y is summable_set 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 not Y1 is empty & Y1 c= Y & Y0 misses Y1 holds

||.(setsum Y1).|| < e ) ) )