theorem Th3: :: NDIFF_5:3

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