for X being RealUnitarySpace
for Y being finite Subset of X st not Y is empty holds
Y is summable_set