theorem Th19: :: LOPBAN_3:19

for X being RealNormSpace
for seq being sequence of X
for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq)