theorem Th29: :: NDIFF_1:29

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