theorem Th12: :: NDIFF_2:12

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 L1 being Lipschitzian LinearOperator of S,T
for L2 being Lipschitzian LinearOperator of T,U holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U