let I be Function of REAL,(REAL 1); :: thesis: for J being Function of (REAL 1),REAL st I = (proj (1,1)) " & J = proj (1,1) holds
( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )
let J be Function of (REAL 1),REAL; :: thesis: ( I = (proj (1,1)) " & J = proj (1,1) implies ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) ) )
assume that
A1: I = (proj (1,1)) " and
A2: J = proj (1,1) ; :: thesis: ( ( for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc ) )
thus for R being RestFunc of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is RestFunc :: thesis: for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc

proof

let R be RestFunc of (REAL-NS 1),(REAL-NS 1); :: thesis: (J * R) * I is RestFunc
A3: R is total by NDIFF_1:def 5;
the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
then reconsider R0 = R as Function of (REAL 1),(REAL 1) by A3;
reconsider R1 = (J * R) * I as PartFunc of REAL,REAL ;
A4: (J * R0) * I is Function of REAL,REAL ;
then A5: dom R1 = REAL by FUNCT_2:def 1;
A6: 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
A7: d > 0 and
A8: for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r by A3, 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
A9: z1 <> 0 and
A10: |.z1.| < d ; :: thesis: (|.z1.| ") * |.(R1 . z1).| < r
reconsider z1 = z1 as Element of REAL by XREAL_0:def 1;
reconsider z = I . z1 as Point of (REAL-NS 1) by REAL_NS1:def 4;
|.z1.| > 0 by A9, COMPLEX1:47;
then ||.z.|| <> 0 by A1, Th3;
then A11: z <> 0. (REAL-NS 1) ;
I * J = id (dom (proj (1,1))) by A1, A2, FUNCT_1:39;
then A12: I * J = id (REAL 1) by FUNCT_2:def 1;
A13: dom (J * R0) = REAL 1 by FUNCT_2:def 1;
R is total by NDIFF_1:def 5;
then A14: dom R = the carrier of (REAL-NS 1) by PARTFUN1:def 2;
then R /. z = R . z by PARTFUN1:def 6;
then R /. z = ((id the carrier of (REAL-NS 1)) * R) . (I . z1) by FUNCT_2:17;
then R /. z = ((I * J) * R) . (I . z1) by A12, REAL_NS1:def 4;
then A15: R /. z = (I * J) . (R . (I . z1)) by A14, FUNCT_1:13;
dom J = REAL 1 by FUNCT_2:def 1;
then R /. z = I . (J . (R0 . z)) by A15, FUNCT_1:13, FUNCT_2:5;
then R /. z = I . ((J * R0) . (I . z1)) by A13, FUNCT_1:12;
then R /. z = I . (R1 . z1) by A5, FUNCT_1:12;
then A16: ||.(R /. z).|| = |.(R1 . z1).| by A1, Th3;
A17: ||.z.|| " = |.z1.| " by A1, Th3;
||.z.|| < d by A1, A10, Th3;
hence (|.z1.| ") * |.(R1 . z1).| < r by A8, A11, A17, A16; :: thesis: verum

end;

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

A18: now :: thesis: for r0 being Real st r0 > 0 holds
ex m being Nat st
for n being Nat st m <= n holds
|.((((h ") (#) (R1 /* h)) . n) - 0).| < r0

let r0 be Real; :: thesis: ( r0 > 0 implies ex m being Nat st
for n being Nat st m <= n holds
|.((((h ") (#) (R1 /* h)) . n) - 0).| < r0 )
reconsider r = r0 as Real ;
A19: lim h = 0 ;
assume r0 > 0 ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
|.((((h ") (#) (R1 /* h)) . n) - 0).| < r0
then consider d being Real such that
A20: d > 0 and
A21: for z1 being Real st z1 <> 0 & |.z1.| < d holds
(|.z1.| ") * |.(R1 . z1).| < r by A6;
reconsider d1 = d as Real ;
consider m being Nat such that
A22: for n being Nat st m <= n holds
|.((h . n) - 0).| < d1 by A20, A19, SEQ_2:def 7;
take m = m; :: thesis: for n being Nat st m <= n holds
|.((((h ") (#) (R1 /* h)) . n) - 0).| < r0

hereby :: thesis: verum

let n be Nat; :: thesis: ( m <= n implies |.((((h ") (#) (R1 /* h)) . n) - 0).| < r0 )
A23: h . n <> 0 by SEQ_1:5;
A24: n in NAT by ORDINAL1:def 12;
rng h c= dom R1 by A5;
then A25: (|.(h . n).| ") * |.(R1 . (h . n)).| = (|.(h . n).| ") * |.((R1 /* h) . n).| by FUNCT_2:108, A24
.= (((abs h) . n) ") * |.((R1 /* h) . n).| by SEQ_1:12
.= (((abs h) ") . n) * |.((R1 /* h) . n).| by VALUED_1:10
.= ((abs (h ")) . n) * |.((R1 /* h) . n).| by SEQ_1:54
.= |.((h ") . n).| * |.((R1 /* h) . n).| by SEQ_1:12
.= |.(((h ") . n) * ((R1 /* h) . n)).| by COMPLEX1:65
.= |.((((h ") (#) (R1 /* h)) . n) - 0).| by SEQ_1:8 ;
assume m <= n ; :: thesis: |.((((h ") (#) (R1 /* h)) . n) - 0).| < r0
then |.((h . n) - 0).| < d by A22;
hence |.((((h ") (#) (R1 /* h)) . n) - 0).| < r0 by A21, A23, A25; :: thesis: verum

end;

end;

hence (h ") (#) (R1 /* h) is convergent by SEQ_2:def 6; :: thesis: lim ((h ") (#) (R1 /* h)) = 0
hence lim ((h ") (#) (R1 /* h)) = 0 by A18, SEQ_2:def 7; :: thesis: verum

end;

hence (J * R) * I is RestFunc by A4, FDIFF_1:def 2; :: thesis: verum

end;

thus for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LinearFunc :: thesis: verum

proof

let L be LinearOperator of (REAL-NS 1),(REAL-NS 1); :: thesis: (J * L) * I is LinearFunc
A26: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
then reconsider L0 = L as Function of (REAL 1),(REAL 1) ;
reconsider L1 = (J * L0) * I as PartFunc of REAL,REAL ;
A27: dom (J * L0) = REAL 1 by FUNCT_2:def 1;
consider r being Real such that
A28: r = L1 . 1 ;
A29: dom ((J * L0) * I) = REAL by FUNCT_2:def 1;
A30: dom L0 = REAL 1 by FUNCT_2:def 1;
for p being Real holds L1 . p = r * p

proof

reconsider 1p = I . jj as VECTOR of (REAL-NS 1) by REAL_NS1:def 4;
let p be Real; :: thesis: L1 . p = r * p
reconsider pp = p, jj = 1 as Element of REAL by XREAL_0:def 1;
dom I = REAL by FUNCT_2:def 1;
then L1 . p = (J * L) . (I . (pp * jj)) by FUNCT_1:13;
then L1 . p = (J * L) . (p * 1p) by A1, Th3;
then L1 . p = J . (L . (p * 1p)) by A26, A30, FUNCT_1:13;
then L1 . p = J . (p * (L . 1p)) by LOPBAN_1:def 5;
then L1 . p = p * (J . (L . 1p)) by A2, Th4;
then L1 . p = p * ((J * L0) . (I . jj)) by A27, FUNCT_1:12;
hence L1 . p = r * p by A29, A28, FUNCT_1:12; :: thesis: verum

end;

hence (J * L) * I is LinearFunc by FDIFF_1:def 3; :: thesis: verum

end;