for X being RealNormSpace
for seq being summable sequence of X
for z being Real holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )