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;

.= 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

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 ) )

dom (R2 * (L + R1)) =
dom (L + R1)
by A5, RELAT_1:27
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;

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;( 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

0 / (1 + ||.r.||) < d / (1 + ||.r.||)
by A11, XREAL_1:74;(|.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;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

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

.= 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