theorem :: NORMSP_1:28

for a being Real
for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
lim (a * S) = a * (lim S)