for X being RealHilbertSpace
for seq being sequence of X st seq is absolutely_summable holds
seq is summable