let n, m be non zero Element of NAT ; :: thesis: 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)
let R1 be RestFunc of (REAL-NS n); :: thesis: ( R1 /. 0 = 0. (REAL-NS n) implies 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) )
assume A1: R1 /. 0 = 0. (REAL-NS n) ; :: thesis: 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)
let R2 be RestFunc of (REAL-NS n),(REAL-NS m); :: thesis: ( R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) implies 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) )
assume A2: R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) ; :: thesis: 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)
let L1 be LinearFunc of (REAL-NS n); :: thesis: for L2 being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m)
let L2 be Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m); :: thesis: (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m)
A3: L2 * R1 is RestFunc of (REAL-NS m) by Th47;
R2 * (L1 + R1) is RestFunc of (REAL-NS m) by A1, A2, Th48;
hence (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of (REAL-NS m) by A3, NDIFF_3:7; :: thesis: verum