theorem Th8: :: NDIFF_3:8

for F being RealNormSpace
for r being Real
for R being RestFunc of F holds r (#) R is RestFunc of F