for D being non empty set
for p, r being Real
for Y being RealNormSpace
for H being Functional_Sequence of D, the carrier of Y holds (r * p) (#) H = r (#) (p (#) H)