theorem :: SEQFUNC2:32

for D being non empty set
for r being Real
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y
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)) )