let S, T, U be RealNormSpace; :: thesis: 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
let R1 be RestFunc of S,T; :: thesis: ( R1 /. (0. S) = 0. T implies 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 )
assume A1: R1 /. (0. S) = 0. T ; :: thesis: 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
let R2 be RestFunc of T,U; :: thesis: ( R2 /. (0. T) = 0. U implies 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 )
assume A2: R2 /. (0. T) = 0. U ; :: thesis: 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
let L1 be Lipschitzian LinearOperator of S,T; :: thesis: for L2 being Lipschitzian LinearOperator of T,U holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U
let L2 be Lipschitzian LinearOperator of T,U; :: thesis: (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U
A3: L2 * R1 is RestFunc of S,U by Th9;
R2 * (L1 + R1) is RestFunc of S,U by A1, A2, Th11;
hence (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of S,U by A3, NDIFF_1:28; :: thesis: verum