theorem Th9: :: NDIFF_2:9

for S, T, U being RealNormSpace
for R being RestFunc of S,T
for L being Lipschitzian LinearOperator of T,U holds L * R is RestFunc of S,U