theorem Th10: :: SERIES_1:10

for r being Real
for s being Real_Sequence st s is summable holds
( r (#) s is summable & Sum (r (#) s) = r * (Sum s) )