let n, m be non zero Element of NAT ; 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); ( 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)
; 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); ( 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)
; 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); 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 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;
( 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
;
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 for hh being Real st hh <> 0 & |.hh.| < min (d0,(d / (1 + ||.r.||))) holds
(|.hh.| ") * ||.((R2 * (L + R1)) /. hh).|| < eelet hh be
Real;
( 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.||)))
;
(|.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;
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;
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; verum