let n be non zero Element of NAT ; :: thesis: for I being Function of REAL,() st I = (proj (1,1)) " holds
( ( for R being RestFunc of (),() holds R * I is RestFunc of () ) & ( for L being LinearOperator of (),() holds L * I is LinearFunc of () ) )

let I be Function of REAL,(); :: thesis: ( I = (proj (1,1)) " implies ( ( for R being RestFunc of (),() holds R * I is RestFunc of () ) & ( for L being LinearOperator of (),() holds L * I is LinearFunc of () ) ) )
assume A1: I = (proj (1,1)) " ; :: thesis: ( ( for R being RestFunc of (),() holds R * I is RestFunc of () ) & ( for L being LinearOperator of (),() holds L * I is LinearFunc of () ) )
thus for R being RestFunc of (),() holds R * I is RestFunc of () :: thesis: for L being LinearOperator of (),() holds L * I is LinearFunc of ()
proof
let R be RestFunc of (),(); :: thesis: R * I is RestFunc of ()
A2: R is total by NDIFF_1:def 5;
reconsider R0 = R as Function of (REAL 1),(REAL n) by ;
reconsider R1 = R * I as PartFunc of REAL,() ;
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 () st z <> 0. () & < d holds
() * ||.(R /. z).|| < r by ;
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 () ;
|.zz.| > 0 by ;
then ||.z.|| <> 0 by ;
then A10: z <> 0. () ;
A11: dom I = REAL by FUNCT_2:def 1;
R is total by NDIFF_1:def 5;
then dom R = the carrier of () by PARTFUN1:def 2;
then R /. z = R . (I . z1) by PARTFUN1:def 6;
then R /. z = R1 . zz by ;
then A12: ||.(R /. z).|| = ||.(R1 /. zz).|| by ;
A13: ||.z.|| " = |.z1.| " by ;
||.z.|| < d by ;
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. () )
proof
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0. () )
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. ())).|| < 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. ())).|| < 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. ())).|| < 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 ;
take n0 = n0; :: thesis: for m being Nat st n0 <= m holds
||.((((h ") (#) (R1 /* h)) . m) - (0. ())).|| < r

hereby :: thesis: verum
let m be Nat; :: thesis: ( n0 <= m implies ||.((((h ") (#) (R1 /* h)) . m) - (0. ())).|| < 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
.= (((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. ())).|| by RLVECT_1:13 ;
assume n0 <= m ; :: thesis: ||.((((h ") (#) (R1 /* h)) . m) - (0. ())).|| < r
then |.((h . m) - 0).| < d by A18;
hence ||.((((h ") (#) (R1 /* h)) . m) - (0. ())).|| < r by ; :: thesis: verum
end;
end;
hence (h ") (#) (R1 /* h) is convergent by NORMSP_1:def 6; :: thesis: lim ((h ") (#) (R1 /* h)) = 0. ()
hence lim ((h ") (#) (R1 /* h)) = 0. () by ; :: thesis: verum
end;
hence R * I is RestFunc of () by ; :: thesis: verum
end;
let L be LinearOperator of (),(); :: thesis: L * I is LinearFunc of ()
reconsider L0 = L as Function of (REAL 1),(REAL n) by ;
reconsider L1 = L0 * I as PartFunc of REAL,() by REAL_NS1:def 4;
reconsider r = L1 . jj as Point of () by FUNCT_2:5;
A22: dom (L0 * I) = REAL by ;
for p being Real holds L1 /. p = p * r
proof
reconsider 1p = I . jj as VECTOR of () ;
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 ;
then L1 . p = L . (p * 1p) by ;
then L1 . p = p * (L /. 1p) by LOPBAN_1:def 5;
then L1 /. p = p * (L /. 1p) by ;
hence L1 /. p = p * r by ; :: thesis: verum
end;
hence L * I is LinearFunc of () by NDIFF_3:def 2; :: thesis: verum