for S, T being RealNormSpace
for r being Real
for R being RestFunc of S,T holds r (#) R is RestFunc of S,T