theorem Th8: :: SEQ_2:8

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