for r being Complex
for s being convergent Complex_Sequence holds lim ((r (#) s) *') = (r *') * ((lim s) *')