for S being RealNormSpace
for rseq being Real_Sequence
for seq being sequence of S st rseq is convergent & seq is convergent holds
lim (rseq (#) seq) = (lim rseq) * (lim seq)