let S, T, U be RealNormSpace; 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; ( 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
; 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; ( 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
; 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; 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; (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; verum