theorem Th5: :: NDIFF_5:5

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