theorem :: SEQFUNC:36

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
for x being Element of D st x in X holds
(r (#) H) # x = r (#) (H # x) by Th32;