let S, T be RealNormSpace; :: thesis: for R1 being RestFunc of S st R1 /. 0 = 0. S holds
for R2 being RestFunc of S,T st R2 /. (0. S) = 0. T holds
for L1 being LinearFunc of S
for L2 being Lipschitzian LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of T
let R1 be RestFunc of S; :: thesis: ( R1 /. 0 = 0. S implies for R2 being RestFunc of S,T st R2 /. (0. S) = 0. T holds
for L1 being LinearFunc of S
for L2 being Lipschitzian LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of T )
assume A1: R1 /. 0 = 0. S ; :: thesis: for R2 being RestFunc of S,T st R2 /. (0. S) = 0. T holds
for L1 being LinearFunc of S
for L2 being Lipschitzian LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of T
let R2 be RestFunc of S,T; :: thesis: ( R2 /. (0. S) = 0. T implies for L1 being LinearFunc of S
for L2 being Lipschitzian LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of T )
assume A2: R2 /. (0. S) = 0. T ; :: thesis: for L1 being LinearFunc of S
for L2 being Lipschitzian LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of T
let L1 be LinearFunc of S; :: thesis: for L2 being Lipschitzian LinearOperator of S,T holds (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of T
let L2 be Lipschitzian LinearOperator of S,T; :: thesis: (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of T
( L2 * R1 is RestFunc of T & R2 * (L1 + R1) is RestFunc of T ) by A1, A2, Th4, Th3;
hence (L2 * R1) + (R2 * (L1 + R1)) is RestFunc of T by NDIFF_3:7; :: thesis: verum