let S, T be RealNormSpace; for R being RestFunc of S
for L being Lipschitzian LinearOperator of S,T holds L * R is RestFunc of T
let R be RestFunc of S; for L being Lipschitzian LinearOperator of S,T holds L * R is RestFunc of T
let L be Lipschitzian LinearOperator of S,T; L * R is RestFunc of T
consider K being Real such that
A1:
0 <= K
and
A2:
for z being Point of S holds ||.(L . z).|| <= K * ||.z.||
by LOPBAN_1:def 8;
dom L = the carrier of S
by FUNCT_2:def 1;
then A3:
rng R c= dom L
;
A4:
R is total
by NDIFF_3:def 1;
then A5:
dom R = REAL
by PARTFUN1:def 2;
now for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < e ) )let e be
Real;
( e > 0 implies ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < e ) ) )assume A6:
e > 0
;
ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < e ) )set e1 =
(e / 2) / (1 + K);
consider d being
Real such that A7:
0 < d
and A8:
for
h being
Real st
h <> 0 &
|.h.| < d holds
(|.h.| ") * ||.(R /. h).|| < (e / 2) / (1 + K)
by A1, A4, A6, Th1;
A9:
e / 2
< e
by A6, XREAL_1:216;
now for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < elet h be
Real;
( h <> 0 & |.h.| < d implies (|.h.| ") * ||.((L * R) /. h).|| < e )reconsider hh =
h as
Element of
REAL by XREAL_0:def 1;
assume A10:
(
h <> 0 &
|.h.| < d )
;
(|.h.| ") * ||.((L * R) /. h).|| < ethen
(|.h.| ") * ||.(R /. h).|| < (e / 2) / (1 + K)
by A8;
then
(K + 1) * ((|.h.| ") * ||.(R /. h).||) <= (K + 1) * ((e / 2) / (1 + K))
by A1, XREAL_1:64;
then A11:
(K + 1) * ((|.h.| ") * ||.(R /. h).||) <= e / 2
by A1, XCMPLX_1:87;
|.h.| <> 0
by A10, COMPLEX1:45;
then A12:
|.h.| > 0
by COMPLEX1:46;
reconsider p0 =
0 ,
p1 = 1 as
Element of
REAL by XREAL_0:def 1;
p0 + K < p1 + K
by XREAL_1:8;
then A13:
K * ||.(R /. h).|| <= (K + 1) * ||.(R /. h).||
by XREAL_1:64;
||.(L . (R /. h)).|| <= K * ||.(R /. h).||
by A2;
then
||.(L . (R /. h)).|| <= (K + 1) * ||.(R /. h).||
by A13, XXREAL_0:2;
then
(|.h.| ") * ||.(L . (R /. h)).|| <= (|.h.| ") * ((K + 1) * ||.(R /. h).||)
by A12, XREAL_1:64;
then A14:
(|.h.| ") * ||.(L . (R /. h)).|| <= e / 2
by A11, XXREAL_0:2;
L . (R /. h) = L /. (R /. h)
;
then
L . (R /. hh) = (L * R) /. hh
by A5, A3, PARTFUN2:5;
hence
(|.h.| ") * ||.((L * R) /. h).|| < e
by A9, A14, XXREAL_0:2;
verum end; hence
ex
d being
Real st
(
d > 0 & ( for
h being
Real st
h <> 0 &
|.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < e ) )
by A7;
verum end;
hence
L * R is RestFunc of T
by A4, Th1; verum