let n be non zero Element of NAT ; :: thesis: 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); :: thesis: ( 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)) " ; :: thesis: ( ( 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) :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( z1 <> 0 & |.z1.| < d implies (|.z1.| ") * ||.(R1 /. z1).|| < r )
assume that
A8: z1 <> 0 and
A9: |.z1.| < d ; :: thesis: (|.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; :: thesis: verum

end;

hence ( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r ) ) by A6; :: thesis: 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) )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0. (REAL-NS n) )

A14: now :: thesis: for r being Real st r > 0 holds
ex n0 being Nat st
for m being Nat st n0 <= m holds
||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r

let r be Real; :: thesis: ( r > 0 implies ex n0 being Nat st
for m being Nat st n0 <= m holds
||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r )
A15: lim h = 0 ;
assume r > 0 ; :: thesis: ex n0 being Nat st
for m being Nat st n0 <= m holds
||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r
then consider d being Real such that
A16: d > 0 and
A17: for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * ||.(R1 /. z1).|| < r by A5;
reconsider d1 = d as Real ;
consider n0 being Nat such that
A18: for m being Nat st n0 <= m holds
|.((h . m) - 0).| < d1 by A16, A15, SEQ_2:def 7;
take n0 = n0; :: thesis: for m being Nat st n0 <= m holds
||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r

hereby :: thesis: verum

let m be Nat; :: thesis: ( n0 <= m implies ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r )
A19: m in NAT by ORDINAL1:def 12;
A20: h . m <> 0 by SEQ_1:5;
rng h c= dom R1 by A4;
then A21: (|.(h . m).| ") * ||.(R1 /. (h . m)).|| = (|.(h . m).| ") * ||.((R1 /* h) . m).|| by A19, FUNCT_2:109
.= (((abs h) . m) ") * ||.((R1 /* h) . m).|| by SEQ_1:12
.= (((abs h) ") . m) * ||.((R1 /* h) . m).|| by VALUED_1:10
.= (|.(h ").| . m) * ||.((R1 /* h) . m).|| by SEQ_1:54
.= |.((h ") . m).| * ||.((R1 /* h) . m).|| by SEQ_1:12
.= ||.(((h ") . m) * ((R1 /* h) . m)).|| by NORMSP_1:def 1
.= ||.(((h ") (#) (R1 /* h)) . m).|| by NDIFF_1:def 2
.= ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| by RLVECT_1:13 ;
assume n0 <= m ; :: thesis: ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r
then |.((h . m) - 0).| < d by A18;
hence ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r by A17, A20, A21; :: thesis: verum

end;

end;

hence (h ") (#) (R1 /* h) is convergent by NORMSP_1:def 6; :: thesis: lim ((h ") (#) (R1 /* h)) = 0. (REAL-NS n)
hence lim ((h ") (#) (R1 /* h)) = 0. (REAL-NS n) by A14, NORMSP_1:def 7; :: thesis: verum

end;

hence R * I is RestFunc of (REAL-NS n) by A3, NDIFF_3:def 1; :: thesis: verum

end;

let L be LinearOperator of (REAL-NS 1),(REAL-NS n); :: thesis: 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

proof

reconsider 1p = I . jj as VECTOR of (REAL-NS 1) ;
let p be Real; :: thesis: L1 /. p = p * r
A23: p in REAL by XREAL_0:def 1;
A24: dom L1 = REAL by FUNCT_2:def 1;
dom I = REAL by FUNCT_2:def 1;
then L1 . p = L0 . (I . (p * 1)) by A23, FUNCT_1:13;
then L1 . p = L . (p * 1p) by A1, Lm1, PDIFF_1:3;
then L1 . p = p * (L /. 1p) by LOPBAN_1:def 5;
then L1 /. p = p * (L /. 1p) by A23, A24, PARTFUN1:def 6;
hence L1 /. p = p * r by A22, FUNCT_1:12; :: thesis: verum

end;

hence L * I is LinearFunc of (REAL-NS n) by NDIFF_3:def 2; :: thesis: verum