let I be Function of REAL,(REAL 1); for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds
( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )
let J be Function of (REAL 1),REAL; ( I = (proj (1,1)) " & J = proj (1,1) implies ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) ) )
assume that
A1:
I = (proj (1,1)) "
and
A2:
J = proj (1,1)
; ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )
thus
for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc
for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFuncproof
let R be
RestFunc of
(REAL-NS 1),
(REAL-NS 1);
(J * R) * I is RestFunc
A3:
R is
total
by NDIFF_1:def 5;
the
carrier of
(REAL-NS 1) = REAL 1
by REAL_NS1:def 4;
then reconsider R0 =
R as
Function of
(REAL 1),
(REAL 1) by A3;
reconsider R1 =
(J * R) * I as
PartFunc of
REAL,
REAL ;
A4:
(J * R0) * I is
Function of
REAL,
REAL
;
then A5:
dom R1 = REAL
by FUNCT_2:def 1;
A6:
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 A7:
d > 0
and A8:
for
z being
Point of
(REAL-NS 1) st
z <> 0. (REAL-NS 1) &
||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r
by A3, 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 A9:
z1 <> 0
and A10:
|.z1.| < d
;
(|.z1.| ") * |.(R1 . z1).| < r
reconsider z1 =
z1 as
Element of
REAL by XREAL_0:def 1;
reconsider z =
I . z1 as
Point of
(REAL-NS 1) by REAL_NS1:def 4;
|.z1.| > 0
by A9, COMPLEX1:47;
then
||.z.|| <> 0
by A1, Th3;
then A11:
z <> 0. (REAL-NS 1)
;
I * J = id (dom (proj (1,1)))
by A1, A2, FUNCT_1:39;
then A12:
I * J = id (REAL 1)
by FUNCT_2:def 1;
A13:
dom (J * R0) = REAL 1
by FUNCT_2:def 1;
R is
total
by NDIFF_1:def 5;
then A14:
dom R = the
carrier of
(REAL-NS 1)
by PARTFUN1:def 2;
then
R /. z = R . z
by PARTFUN1:def 6;
then
R /. z = ((id the carrier of (REAL-NS 1)) * R) . (I . z1)
by FUNCT_2:17;
then
R /. z = ((I * J) * R) . (I . z1)
by A12, REAL_NS1:def 4;
then A15:
R /. z = (I * J) . (R . (I . z1))
by A14, FUNCT_1:13;
dom J = REAL 1
by FUNCT_2:def 1;
then
R /. z = I . (J . (R0 . z))
by A15, FUNCT_1:13, FUNCT_2:5;
then
R /. z = I . ((J * R0) . (I . z1))
by A13, FUNCT_1:12;
then
R /. z = I . (R1 . z1)
by A5, FUNCT_1:12;
then A16:
||.(R /. z).|| = |.(R1 . z1).|
by A1, Th3;
A17:
||.z.|| " = |.z1.| "
by A1, Th3;
||.z.|| < d
by A1, A10, Th3;
hence
(|.z1.| ") * |.(R1 . z1).| < r
by A8, A11, A17, A16;
verum
end;
hence
(
d > 0 & ( for
z1 being
Real st
z1 <> 0 &
|.z1.| < d holds
(|.z1.| ") * |.(R1 . z1).| < r ) )
by A7;
verum
end;
for
h being
non-zero 0 -convergent Real_Sequence holds
(
(h ") (#) (R1 /* h) is
convergent &
lim ((h ") (#) (R1 /* h)) = 0 )
hence
(J * R) * I is
RestFunc
by A4, FDIFF_1:def 2;
verum
end;
thus
for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc
verum