theorem Th39: :: TOPRNS_1:39

for N being Nat
for r being Real
for seq being Real_Sequence of N st seq is convergent holds
lim (r * seq) = r * (lim seq)