for D being non empty set
for r being Real
for H being Functional_Sequence of D,REAL
for X being set st H is_point_conv_on X holds
( r (#) H is_point_conv_on X & lim ((r (#) H),X) = r (#) (lim (H,X)) )