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 L being Lipschitzian LinearOperator of S,T holds R2 * (L + 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 L being Lipschitzian LinearOperator of S,T holds R2 * (L + R1) is RestFunc of S,U )
assume R1 /. (0. S) = 0. T ; :: thesis: for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
for L being Lipschitzian LinearOperator of S,T holds R2 * (L + R1) is RestFunc of S,U
then consider d0 being Real such that
A1: 0 < d0 and
A2: for h being Point of S st ||.h.|| < d0 holds
||.(R1 /. h).|| <= 1 * ||.h.|| by Th7;
let R2 be RestFunc of T,U; :: thesis: ( R2 /. (0. T) = 0. U implies for L being Lipschitzian LinearOperator of S,T holds R2 * (L + R1) is RestFunc of S,U )
assume A3: R2 /. (0. T) = 0. U ; :: thesis: for L being Lipschitzian LinearOperator of S,T holds R2 * (L + R1) is RestFunc of S,U
let L be Lipschitzian LinearOperator of S,T; :: thesis: R2 * (L + R1) is RestFunc of S,U
consider K being Real such that
A4: 0 <= K and
A5: for h being Point of S holds ||.(L . h).|| <= K * ||.h.|| by LOPBAN_1:def 8;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of T by PARTFUN1:def 2;
then A6: rng (L + R1) c= dom R2 ;
R1 is total by NDIFF_1:def 5;
then A7: L + R1 is total by VFUNCT_1:32;
then A8: dom (L + R1) = the carrier of S by PARTFUN1:def 2;

A9: now :: thesis: for ee being Real st ee > 0 holds
ex dd1 being Real st
( dd1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < dd1 holds
(||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) )

let ee be Real; :: thesis: ( ee > 0 implies ex dd1 being Real st
( dd1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < dd1 holds
(||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) ) )
assume A10: ee > 0 ; :: thesis: ex dd1 being Real st
( dd1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < dd1 holds
(||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) )
set e = ee / 2;
A11: ee / 2 < ee by A10, XREAL_1:216;
set e1 = (ee / 2) / (1 + K);
ee / 2 > 0 by A10, XREAL_1:215;
then 0 / (1 + K) < (ee / 2) / (1 + K) by A4, XREAL_1:74;
then consider d being Real such that
A12: 0 < d and
A13: for z being Point of T st ||.z.|| < d holds
||.(R2 /. z).|| <= ((ee / 2) / (1 + K)) * ||.z.|| by A3, Th7;
set d1 = d / (1 + K);
set dd1 = min (d0,(d / (1 + K)));
A14: min (d0,(d / (1 + K))) <= d / (1 + K) by XXREAL_0:17;
A15: min (d0,(d / (1 + K))) <= d0 by XXREAL_0:17;

A16: now :: thesis: for h being Point of S st h <> 0. S & ||.h.|| < min (d0,(d / (1 + K))) holds
(||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee

let h be Point of S; :: thesis: ( h <> 0. S & ||.h.|| < min (d0,(d / (1 + K))) implies (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee )
assume that
A17: h <> 0. S and
A18: ||.h.|| < min (d0,(d / (1 + K))) ; :: thesis: (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee
||.h.|| < d0 by A15, A18, XXREAL_0:2;
then A19: ||.(R1 /. h).|| <= 1 * ||.h.|| by A2;
||.(L . h).|| <= K * ||.h.|| by A5;
then ( ||.((L . h) + (R1 /. h)).|| <= ||.(L . h).|| + ||.(R1 /. h).|| & ||.(L . h).|| + ||.(R1 /. h).|| <= (K * ||.h.||) + (1 * ||.h.||) ) by A19, NORMSP_1:def 1, XREAL_1:7;
then A20: ||.((L . h) + (R1 /. h)).|| <= (K + 1) * ||.h.|| by XXREAL_0:2;
||.h.|| < d / (1 + K) by A14, A18, XXREAL_0:2;
then (K + 1) * ||.h.|| < (K + 1) * (d / (1 + K)) by A4, XREAL_1:68;
then ||.((L . h) + (R1 /. h)).|| < (K + 1) * (d / (1 + K)) by A20, XXREAL_0:2;
then ||.((L . h) + (R1 /. h)).|| < d by A4, XCMPLX_1:87;
then A21: ||.(R2 /. ((L . h) + (R1 /. h))).|| <= ((ee / 2) / (1 + K)) * ||.((L . h) + (R1 /. h)).|| by A13;
((ee / 2) / (1 + K)) * ||.((L . h) + (R1 /. h)).|| <= ((ee / 2) / (1 + K)) * ((K + 1) * ||.h.||) by A4, A10, A20, XREAL_1:64;
then A22: ||.(R2 /. ((L . h) + (R1 /. h))).|| <= ((ee / 2) / (1 + K)) * ((K + 1) * ||.h.||) by A21, XXREAL_0:2;
A23: R2 /. ((L . h) + (R1 /. h)) = R2 /. ((L /. h) + (R1 /. h))
.= R2 /. ((L + R1) /. h) by A8, VFUNCT_1:def 1
.= (R2 * (L + R1)) /. h by A8, A6, PARTFUN2:5 ;
A24: ||.h.|| <> 0 by A17, NORMSP_0:def 5;
then ||.h.|| > 0 by NORMSP_1:4;
then (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| <= (||.h.|| ") * ((((ee / 2) / (1 + K)) * (K + 1)) * ||.h.||) by A23, A22, XREAL_1:64;
then (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| <= ((||.h.|| * (||.h.|| ")) * ((ee / 2) / (1 + K))) * (K + 1) ;
then (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| <= (1 * ((ee / 2) / (1 + K))) * (K + 1) by A24, XCMPLX_0:def 7;
then (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| <= ee / 2 by A4, XCMPLX_1:87;
hence (||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee by A11, XXREAL_0:2; :: thesis: verum

end;

0 / (1 + K) < d / (1 + K) by A4, A12, XREAL_1:74;
then 0 < min (d0,(d / (1 + K))) by A1, XXREAL_0:15;
hence ex dd1 being Real st
( dd1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < dd1 holds
(||.h.|| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) ) by A16; :: thesis: verum

end;

dom (R2 * (L + R1)) = dom (L + R1) by A6, RELAT_1:27
.= the carrier of S by A7, PARTFUN1:def 2 ;
then R2 * (L + R1) is total by PARTFUN1:def 2;
hence R2 * (L + R1) is RestFunc of S,U by A9, NDIFF_1:23; :: thesis: verum