let n be non empty 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: abs z1 < d ; :: thesis: (|.z1.| ") * ||.(R1 /. z1).|| < r
reconsider z = I . z1 as Point of (REAL-NS 1) ;
z1 in REAL ;
then reconsider z1r = z1 as R_eal by NUMBERS:31;
0 < |.z1r.| by A8, EXTREAL2:4;
then abs z1 > 0 by EXTREAL2:1;
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 . z1 by A11, FUNCT_1:13;
then A12: ||.(R /. z).|| = ||.(R1 /. z1).|| by A4, PARTFUN1:def 6;
A13: ||.z.|| " = (abs 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 Element of NAT st
for m being Element of 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 Element of NAT st
for m being Element of 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 Element of NAT st
for m being Element of 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 number ;
consider n0 being Element of NAT such that
A18: for m being Element of NAT st n0 <= m holds
abs ((h . m) - 0) < d1 by A16, A15, SEQ_2:def 7;
take n0 = n0; :: thesis: for m being Element of NAT st n0 <= m holds
||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r

hereby :: thesis: verum

let m be Element of NAT ; :: thesis: ( n0 <= m implies ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r )
A19: h . m <> 0 by SEQ_1:5;
rng h c= dom R1 by A4;
then A20: ((abs (h . m)) ") * ||.(R1 /. (h . m)).|| = ((abs (h . m)) ") * ||.((R1 /* h) . m).|| by FUNCT_2:109
.= (((abs h) . m) ") * ||.((R1 /* h) . m).|| by SEQ_1:12
.= (((abs h) ") . m) * ||.((R1 /* h) . m).|| by VALUED_1:10
.= ((abs (h ")) . m) * ||.((R1 /* h) . m).|| by SEQ_1:54
.= (abs ((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 abs ((h . m) - 0) < d by A18;
hence ||.((((h ") (#) (R1 /* h)) . m) - (0. (REAL-NS n))).|| < r by A17, A19, A20; :: 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 . 1 as Point of (REAL-NS n) by FUNCT_2:5;
A21: dom (L0 * I) = REAL by Lm1, FUNCT_2:def 1;
for p being Real holds L1 . p = p * r

proof

reconsider 1p = I . 1 as VECTOR of (REAL-NS 1) ;
let p be Real; :: thesis: L1 . p = p * r
dom I = REAL by FUNCT_2:def 1;
then L1 . p = L . (I . (p * 1)) by 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;
hence L1 . p = p * r by A21, FUNCT_1:12; :: thesis: verum

end;

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