for f being PartFunc of REAL,REAL
for r being Real st f is convergent_in+infty holds
( r (#) f is convergent_in+infty & lim_in+infty (r (#) f) = r * (lim_in+infty f) )