let n be non zero Element of NAT ; for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds
( ( for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) )
let I be Function of REAL,(REAL-NS 1); ( I = (proj (1,1)) " implies ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) ) )
assume A1:
I = (proj (1,1)) "
; ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n) ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n) ) )
thus
for R being RestFunc of (REAL-NS 1),(REAL-NS n) holds R * I is RestFunc of (REAL-NS n)
for L being LinearOperator of (REAL-NS 1),(REAL-NS n) holds L * I is LinearFunc of (REAL-NS n)proof
let R be
RestFunc of
(REAL-NS 1),
(REAL-NS n);
R * I is RestFunc of (REAL-NS n)
A2:
R is
total
by NDIFF_1:def 5;
reconsider R0 =
R as
Function of
(REAL 1),
(REAL n) by A2, Lm1, REAL_NS1:def 4;
reconsider R1 =
R * I as
PartFunc of
REAL,
(REAL-NS n) ;
A3:
R0 * I is
Function of
REAL,
(REAL n)
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)
;
A11:
dom I = REAL
by FUNCT_2:def 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 A11, 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. (REAL-NS n) )
hence
R * I is
RestFunc of
(REAL-NS n)
by A3, NDIFF_3:def 1;
verum
end;
let L be LinearOperator of (REAL-NS 1),(REAL-NS n); L * I is LinearFunc of (REAL-NS n)
reconsider L0 = L as Function of (REAL 1),(REAL n) by Lm1, REAL_NS1:def 4;
reconsider L1 = L0 * I as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
reconsider r = L1 . jj as Point of (REAL-NS n) by FUNCT_2:5;
A22:
dom (L0 * I) = REAL
by Lm1, FUNCT_2:def 1;
for p being Real holds L1 /. p = p * r
hence
L * I is LinearFunc of (REAL-NS n)
by NDIFF_3:def 2; verum