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