for N being Nat
for r being Real
for seq being Real_Sequence of N st seq is convergent holds
r * seq is convergent