theorem Th32: :: SEQFUNC2:23

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