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

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