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 summable_set holds
for L being linear-Functional of X st L is Lipschitzian holds
Y is_summable_set_by L by Th3, Th7;