let Y be RealNormSpace; for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds
( ( for R being RestFunc of (REAL-NS 1),Y holds R * I is RestFunc of Y ) & ( for L being LinearOperator of (REAL-NS 1),Y holds L * I is LinearFunc of Y ) )
let I be Function of REAL,(REAL-NS 1); ( I = (proj (1,1)) " implies ( ( for R being RestFunc of (REAL-NS 1),Y holds R * I is RestFunc of Y ) & ( for L being LinearOperator of (REAL-NS 1),Y holds L * I is LinearFunc of Y ) ) )
assume A1:
I = (proj (1,1)) "
; ( ( for R being RestFunc of (REAL-NS 1),Y holds R * I is RestFunc of Y ) & ( for L being LinearOperator of (REAL-NS 1),Y holds L * I is LinearFunc of Y ) )
A0:
dom I = REAL
by FUNCT_2:def 1;
thus
for R being RestFunc of (REAL-NS 1),Y holds R * I is RestFunc of Y
for L being LinearOperator of (REAL-NS 1),Y holds L * I is LinearFunc of Yproof
let R be
RestFunc of
(REAL-NS 1),
Y;
R * I is RestFunc of Y
A2:
R is
total
by NDIFF_1:def 5;
then reconsider R0 =
R as
Function of
(REAL 1),
Y by Lm1;
reconsider R1 =
R * I as
PartFunc of
REAL,
Y ;
A3:
R0 * I is
Function of
REAL,
Y
by Lm1;
then A4:
dom R1 = REAL
by FUNCT_2:def 1;
A5:
for
r being
Real st
r > 0 holds
ex
d being
Real st
(
d > 0 & ( for
z1 being
Real st
z1 <> 0 &
|.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r ) )
proof
let r be
Real;
( r > 0 implies ex d being Real st
( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r ) ) )
assume
r > 0
;
ex d being Real st
( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r ) )
then consider d being
Real such that A6:
d > 0
and A7:
for
z being
Point of
(REAL-NS 1) st
z <> 0. (REAL-NS 1) &
||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r
by A2, NDIFF_1:23;
take
d
;
( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r ) )
for
z1 being
Real st
z1 <> 0 &
|.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r
proof
let z1 be
Real;
( z1 <> 0 & |.z1.| < d implies (|.z1.| ") * ||.(R1 /. z1).|| < r )
assume that A8:
z1 <> 0
and A9:
|.z1.| < d
;
(|.z1.| ") * ||.(R1 /. z1).|| < r
reconsider zz =
z1 as
Element of
REAL by XREAL_0:def 1;
reconsider z =
I . zz as
Point of
(REAL-NS 1) ;
|.zz.| > 0
by A8, COMPLEX1:47;
then
||.z.|| <> 0
by A1, Lm1, PDIFF_1:3;
then A10:
z <> 0. (REAL-NS 1)
;
R is
total
by NDIFF_1:def 5;
then
dom R = the
carrier of
(REAL-NS 1)
by PARTFUN1:def 2;
then
R /. z = R . (I . z1)
by PARTFUN1:def 6;
then
R /. z = R1 . zz
by A0, FUNCT_1:13;
then A12:
||.(R /. z).|| = ||.(R1 /. zz).||
by A4, PARTFUN1:def 6;
A13:
||.z.|| " = |.z1.| "
by A1, Lm1, PDIFF_1:3;
||.z.|| < d
by A1, A9, Lm1, PDIFF_1:3;
hence
(|.z1.| ") * ||.(R1 /. z1).|| < r
by A7, A10, A13, A12;
verum
end;
hence
(
d > 0 & ( for
z1 being
Real st
z1 <> 0 &
|.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r ) )
by A6;
verum
end;
for
h being
non-zero 0 -convergent Real_Sequence holds
(
(h ") (#) (R1 /* h) is
convergent &
lim ((h ") (#) (R1 /* h)) = 0. Y )
hence
R * I is
RestFunc of
Y
by A3, NDIFF_3:def 1;
verum
end;
let L be LinearOperator of (REAL-NS 1),Y; L * I is LinearFunc of Y
reconsider L0 = L as Function of (REAL 1),Y by Lm1;
reconsider L1 = L0 * I as PartFunc of REAL,Y ;
reconsider r = L1 . jj as Point of Y by FUNCT_2:5;
A22:
( dom (L0 * I) = REAL & dom L1 = REAL )
by FUNCT_2:def 1;
for p being Real holds L1 /. p = p * r
hence
L * I is LinearFunc of Y
by NDIFF_3:def 2; verum