theorem Th9: :: SERIES_1:9

for r being Real
for s being Real_Sequence holds Partial_Sums (r (#) s) = r (#) (Partial_Sums s)