theorem Th7: :: BHSP_6:7

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 Subset of X st Y is weakly_summable_set holds

for L being linear-Functional of X st L is Lipschitzian holds

Y is_summable_set_by L

for Y being Subset of X st Y is weakly_summable_set holds

for L being linear-Functional of X st L is Lipschitzian holds

Y is_summable_set_by L