let n, m be non zero Element of NAT ; for R being RestFunc of (REAL-NS n)
for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m)
let R be RestFunc of (REAL-NS n); for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m)
let L be Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m); L * R is RestFunc of (REAL-NS m)
set S = REAL-NS n;
set T = REAL-NS m;
consider K being Real such that
A1:
0 <= K
and
A2:
for z being Point of (REAL-NS n) holds ||.(L . z).|| <= K * ||.z.||
by LOPBAN_1:def 8;
dom L = the carrier of (REAL-NS n)
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;
reconsider p0 = 0 , p1 = 1 as Real ;
A6:
p0 + K < p1 + K
by XREAL_1:8;
now for ee being Real st ee > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < ee ) )let ee be
Real;
( ee > 0 implies ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < ee ) ) )assume A7:
ee > 0
;
ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < ee ) )set e =
ee / 2;
ee / 2
> 0
by A7, XREAL_1:215;
then A8:
0 / (1 + K) < (ee / 2) / (1 + K)
by A1, XREAL_1:74;
set e1 =
(ee / 2) / (1 + K);
consider d being
Real such that A9:
0 < d
and A10:
for
h being
Real st
h <> 0 &
|.h.| < d holds
(|.h.| ") * ||.(R /. h).|| < (ee / 2) / (1 + K)
by A4, A8, Th23;
A11:
ee / 2
< ee
by A7, XREAL_1:216;
now for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < eelet h be
Real;
( h <> 0 & |.h.| < d implies (|.h.| ") * ||.((L * R) /. h).|| < ee )assume that A12:
h <> 0
and A13:
|.h.| < d
;
(|.h.| ") * ||.((L * R) /. h).|| < eereconsider hh =
h as
Element of
REAL by XREAL_0:def 1;
(|.h.| ") * ||.(R /. h).|| < (ee / 2) / (1 + K)
by A10, A12, A13;
then
(K + 1) * ((|.h.| ") * ||.(R /. h).||) <= (K + 1) * ((ee / 2) / (1 + K))
by A1, XREAL_1:64;
then A14:
(K + 1) * ((|.h.| ") * ||.(R /. h).||) <= ee / 2
by A1, XCMPLX_1:87;
|.h.| <> 0
by A12, COMPLEX1:45;
then A15:
|.h.| > 0
by COMPLEX1:46;
A16:
K * ||.(R /. h).|| <= (K + 1) * ||.(R /. h).||
by A6, XREAL_1:64;
||.(L /. (R /. h)).|| <= K * ||.(R /. h).||
by A2;
then
||.(L /. (R /. h)).|| <= (K + 1) * ||.(R /. h).||
by A16, XXREAL_0:2;
then
(|.h.| ") * ||.(L /. (R /. h)).|| <= (|.h.| ") * ((K + 1) * ||.(R /. h).||)
by A15, XREAL_1:64;
then A17:
(|.h.| ") * ||.(L /. (R /. h)).|| <= ee / 2
by A14, XXREAL_0:2;
L /. (R /. h) =
L /. (R /. hh)
.=
(L * R) /. hh
by A5, A3, PARTFUN2:5
;
hence
(|.h.| ") * ||.((L * R) /. h).|| < ee
by A11, A17, 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).|| < ee ) )
by A9;
verum end;
hence
L * R is RestFunc of (REAL-NS m)
by A4, Th23; verum