for a being Real
for X being RealUnitarySpace
for seq being sequence of X st seq is summable holds
( a * seq is summable & Sum (a * seq) = a * (Sum seq) )