let Y be RealNormSpace; :: thesis: for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds
( ( for R being RestFunc of (REAL-NS 1),Y holds R * I is RestFunc of Y ) & ( for L being LinearOperator of (REAL-NS 1),Y holds L * I is LinearFunc of Y ) )
let I be Function of REAL,(REAL-NS 1); :: thesis: ( I = (proj (1,1)) " implies ( ( for R being RestFunc of (REAL-NS 1),Y holds R * I is RestFunc of Y ) & ( for L being LinearOperator of (REAL-NS 1),Y holds L * I is LinearFunc of Y ) ) )
assume A1: I = (proj (1,1)) " ; :: thesis: ( ( for R being RestFunc of (REAL-NS 1),Y holds R * I is RestFunc of Y ) & ( for L being LinearOperator of (REAL-NS 1),Y holds L * I is LinearFunc of Y ) )
A0: dom I = REAL by FUNCT_2:def 1;
thus for R being RestFunc of (REAL-NS 1),Y holds R * I is RestFunc of Y :: thesis: for L being LinearOperator of (REAL-NS 1),Y holds L * I is LinearFunc of Y

proof

let R be RestFunc of (REAL-NS 1),Y; :: thesis: R * I is RestFunc of Y
A2: R is total by NDIFF_1:def 5;
then reconsider R0 = R as Function of (REAL 1),Y by Lm1;
reconsider R1 = R * I as PartFunc of REAL,Y ;
A3: R0 * I is Function of REAL,Y 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) ;
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 A0, 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. Y )

proof

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

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. Y)).|| < 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. Y)).|| < 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. Y)).|| < 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. Y)).|| < r

hereby :: thesis: verum

let m be Nat; :: thesis: ( n0 <= m implies ||.((((h ") (#) (R1 /* h)) . m) - (0. Y)).|| < r )
A19: m in NAT by ORDINAL1:def 12;
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) - (0. Y)).|| by NDIFF_1:def 2 ;
assume n0 <= m ; :: thesis: ||.((((h ") (#) (R1 /* h)) . m) - (0. Y)).|| < r
then |.((h . m) - 0).| < d by A18;
hence ||.((((h ") (#) (R1 /* h)) . m) - (0. Y)).|| < r by A17, SEQ_1:5, A21; :: thesis: verum

end;

end;

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

end;

hence R * I is RestFunc of Y by A3, NDIFF_3:def 1; :: thesis: verum

end;

let L be LinearOperator of (REAL-NS 1),Y; :: thesis: L * I is LinearFunc of Y
reconsider L0 = L as Function of (REAL 1),Y by Lm1;
reconsider L1 = L0 * I as PartFunc of REAL,Y ;
reconsider r = L1 . jj as Point of Y by FUNCT_2:5;
A22: ( dom (L0 * I) = REAL & dom L1 = REAL ) by 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
L1 . p = L0 . (I . (p * 1)) by A0, XREAL_0:def 1, 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 XREAL_0:def 1, A22, PARTFUN1:def 6;
hence L1 /. p = p * r by A22, FUNCT_1:12; :: thesis: verum

end;

hence L * I is LinearFunc of Y by NDIFF_3:def 2; :: thesis: verum