for S being RealNormSpace
for h being sequence of S
for r being Real holds r (#) h = r * h