let S, T be RealNormSpace; 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; ( 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
; 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; ( 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
; for L being LinearFunc of S holds R2 * (L + R1) is RestFunc of T
let L be LinearFunc of S; 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 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;
( 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
;
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 for hh being Real st hh <> 0 & |.hh.| < min (d0,(d / (1 + K))) holds
(|.hh.| ") * ||.((R2 * (L + R1)) /. hh).|| < elet hh be
Real;
( 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)))
;
(|.hh.| ") * ||.((R2 * (L + R1)) /. hh).|| < ereconsider 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;
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;
verum end;
hence
R2 * (L + R1) is RestFunc of T
by A7, Th1; verum