for E being RealNormSpace
for a being Point of E
for f being convergent Real_Sequence holds lim (f * a) = (lim f) * a