theorem Th49: :: NDIFF_4:49

for n, m being non zero Element of NAT
for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds
for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds
for L1 being LinearFunc of (REAL-NS n)
for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m)