for S, T being RealNormSpace
for h being PartFunc of S,T
for seq being sequence of S
for r being Real st h is total holds
(r (#) h) /* seq = r * (h /* seq)