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

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

( ( 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 L be LinearOperator of (REAL-NS 1),Y; :: thesis: L * I is LinearFunc of Y
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 ) )

( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0. Y )

end;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

for h being non-zero 0 -convergent Real_Sequence holds
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

(|.z1.| ") * ||.(R1 /. z1).|| < r ) ) by A6; :: thesis: verum

end;( 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

hence
( d > 0 & ( for z1 being Real st z1 <> 0 & |.z1.| < d holds
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;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

(|.z1.| ") * ||.(R1 /. z1).|| < r ) ) by A6; :: thesis: verum

( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0. Y )

proof

hence
R * I is RestFunc of Y
by A3, NDIFF_3:def 1; :: thesis: verum
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0. Y )

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

end;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

hence
(h ") (#) (R1 /* h) is convergent
; :: thesis: lim ((h ") (#) (R1 /* h)) = 0. Yex 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

end;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;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

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

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

hence
L * I is LinearFunc of Y
by NDIFF_3:def 2; :: thesis: verum
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;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