theorem Th19: :: CLOPBAN3:19

for X being ComplexNormSpace
for seq being sequence of X
for z being Complex holds Partial_Sums (z * seq) = z * (Partial_Sums seq)