for X being RealUnitarySpace
for seq being sequence of X st seq is summable holds
Partial_Sums seq is bounded ;