theorem :: NDIFF_2:8

for S, T, U being RealNormSpace
for R being RestFunc of T,U st R /. (0. T) = 0. U holds
for L being Lipschitzian LinearOperator of S,T holds R * L is RestFunc of S,U