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

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

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

A13: now :: thesis: for hh being Real st hh <> 0 & |.hh.| < min (d0,(d / (1 + K))) holds
(|.hh.| ") * ||.((R2 * (L + R1)) /. hh).|| < e

let hh be Real; :: thesis: ( hh <> 0 & |.hh.| < min (d0,(d / (1 + K))) implies (|.hh.| ") * ||.((R2 * (L + R1)) /. hh).|| < e )
assume that
A14: hh <> 0 and
A15: |.hh.| < min (d0,(d / (1 + K))) ; :: thesis: (|.hh.| ") * ||.((R2 * (L + R1)) /. hh).|| < e
reconsider h = hh as Element of REAL by XREAL_0:def 1;
|.h.| < d0 by A12, A15, XXREAL_0:2;
then A16: ||.(R1 /. h).|| <= 1 * |.h.| by A2;
reconsider p0 = 0 as Element of REAL by XREAL_0:def 1;
L . h = L /. h
.= h * r by A4 ;
then (||.(L . h).|| - (K * |.h.|)) + (K * |.h.|) <= p0 + (K * |.h.|) by NORMSP_1:def 1;
then ( ||.((L . h) + (R1 /. h)).|| <= ||.(L . h).|| + ||.(R1 /. h).|| & ||.(L . h).|| + ||.(R1 /. h).|| <= (K * |.h.|) + (1 * |.h.|) ) by A16, NORMSP_1:def 1, XREAL_1:7;
then A17: ||.((L . h) + (R1 /. h)).|| <= (K + 1) * |.h.| by XXREAL_0:2;
then A18: ((e / 2) / (1 + K)) * ||.((L . h) + (R1 /. h)).|| <= ((e / 2) / (1 + K)) * ((K + 1) * |.h.|) by A8, XREAL_1:64;
|.h.| < d / (1 + K) by A12, A15, XXREAL_0:2;
then (K + 1) * |.h.| < (K + 1) * (d / (1 + K)) by XREAL_1:68;
then ||.((L . h) + (R1 /. h)).|| < (K + 1) * (d / (1 + K)) by A17, XXREAL_0:2;
then ||.((L . h) + (R1 /. h)).|| < d by XCMPLX_1:87;
then ||.(R2 /. ((L . h) + (R1 /. h))).|| <= ((e / 2) / (1 + K)) * ||.((L . h) + (R1 /. h)).|| by A11;
then A19: ||.(R2 /. ((L . h) + (R1 /. h))).|| <= ((e / 2) / (1 + K)) * ((K + 1) * |.h.|) by A18, XXREAL_0:2;
A20: R2 /. ((L . h) + (R1 /. h)) = R2 /. ((L /. h) + (R1 /. h))
.= R2 /. ((L + R1) /. h) by A6, VFUNCT_1:def 1
.= (R2 * (L + R1)) /. h by A6, A5, PARTFUN2:5 ;
A21: |.h.| <> 0 by A14, COMPLEX1:45;
then |.h.| > 0 by COMPLEX1:46;
then (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| <= (|.h.| ") * ((((e / 2) / (1 + K)) * (K + 1)) * |.h.|) by A20, A19, XREAL_1:64;
then (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| <= ((|.h.| * (|.h.| ")) * ((e / 2) / (1 + K))) * (K + 1) ;
then (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| <= (1 * ((e / 2) / (1 + K))) * (K + 1) by A21, XCMPLX_0:def 7;
then (|.h.| ") * ||.((R2 * (L + R1)) /. h).|| <= e / 2 by XCMPLX_1:87;
hence (|.hh.| ") * ||.((R2 * (L + R1)) /. hh).|| < e by A9, XXREAL_0:2; :: thesis: verum

end;

0 < min (d0,(d / (1 + K))) by A1, A10, XXREAL_0:15;
hence ex dd1 being Real st
( dd1 > 0 & ( for h being Real st h <> 0 & |.h.| < dd1 holds
(|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < e ) ) by A13; :: thesis: verum

end;

hence R2 * (L + R1) is RestFunc of T by A7, Th1; :: thesis: verum