theorem Th7: :: SEQ_2:7

for r being Real
for seq being Real_Sequence st seq is convergent holds
r (#) seq is convergent