theorem Th11: :: NDIFF_2:11

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