for F being RealNormSpace
for r being Real
for L being LinearFunc of F holds r (#) L is LinearFunc of F