theorem Th3: :: CLVECT_3:3

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