let n, m be non zero Element of NAT ; :: thesis: for R1 being RestFunc of (REAL-NS n) st R1 /. 0 = 0. (REAL-NS n) holds
for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds
for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m)
set S = REAL-NS n;
set T = REAL-NS m;
let R1 be RestFunc of (REAL-NS n); :: thesis: ( R1 /. 0 = 0. (REAL-NS n) implies for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds
for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m) )
assume R1 /. 0 = 0. (REAL-NS n) ; :: thesis: for R2 being RestFunc of (REAL-NS n),(REAL-NS m) st R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) holds
for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m)
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 Th46;
let R2 be RestFunc of (REAL-NS n),(REAL-NS m); :: thesis: ( R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) implies for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m) )
assume A3: R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) ; :: thesis: for L being LinearFunc of (REAL-NS n) holds R2 * (L + R1) is RestFunc of (REAL-NS m)
let L be LinearFunc of (REAL-NS n); :: thesis: R2 * (L + R1) is RestFunc of (REAL-NS m)
consider r being Point of (REAL-NS n) such that
A4: for h being Real holds L /. h = h * r by NDIFF_3:def 2;
set K = ||.r.||;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of (REAL-NS n) by PARTFUN1:def 2;
then A5: rng (L + R1) c= dom R2 ;
R1 is total by NDIFF_3:def 1;
then A6: L + R1 is total by VFUNCT_1:32;
then A7: dom (L + R1) = REAL by PARTFUN1:def 2;

A8: now :: thesis: for ee being Real st ee > 0 holds
ex dd1 being Real st
( dd1 > 0 & ( for h being Real st h <> 0 & |.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 Real st h <> 0 & |.h.| < dd1 holds
(|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) ) )
assume A9: ee > 0 ; :: thesis: ex dd1 being Real st
( dd1 > 0 & ( for h being Real st h <> 0 & |.h.| < dd1 holds
(|.h.| ") * ||.((R2 * (L + R1)) /. h).|| < ee ) )
set e = ee / 2;
A10: ee / 2 < ee by A9, XREAL_1:216;
set e1 = (ee / 2) / (1 + ||.r.||);
ee / 2 > 0 by A9, XREAL_1:215;
then 0 / (1 + ||.r.||) < (ee / 2) / (1 + ||.r.||) by XREAL_1:74;
then consider d being Real such that
A11: 0 < d and
A12: for z being Point of (REAL-NS n) st ||.z.|| < d holds
||.(R2 /. z).|| <= ((ee / 2) / (1 + ||.r.||)) * ||.z.|| by A3, NDIFF_2:7;
set d1 = d / (1 + ||.r.||);
set dd1 = min (d0,(d / (1 + ||.r.||)));
A13: min (d0,(d / (1 + ||.r.||))) <= d / (1 + ||.r.||) by XXREAL_0:17;
A14: min (d0,(d / (1 + ||.r.||))) <= d0 by XXREAL_0:17;

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

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

end;

0 / (1 + ||.r.||) < d / (1 + ||.r.||) by A11, XREAL_1:74;
then 0 < min (d0,(d / (1 + ||.r.||))) by A1, 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).|| < ee ) ) by A15; :: thesis: verum

end;

dom (R2 * (L + R1)) = dom (L + R1) by A5, RELAT_1:27
.= REAL by A6, PARTFUN1:def 2 ;
then R2 * (L + R1) is total by PARTFUN1:def 2;
hence R2 * (L + R1) is RestFunc of (REAL-NS m) by A8, Th23; :: thesis: verum