for a being Real
for X being RealUnitarySpace
for seq being sequence of X st seq is absolutely_summable holds
a * seq is absolutely_summable