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 REST of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is REST ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LINEAR ) )
let J be Function of (REAL 1),REAL ; :: thesis: ( I = (proj 1,1) " & J = proj 1,1 implies ( ( for R being REST of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is REST ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LINEAR ) ) )
assume A1: ( I = (proj 1,1) " & J = proj 1,1 ) ; :: thesis: ( ( for R being REST of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is REST ) & ( for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LINEAR ) )
thus for R being REST of (REAL-NS 1),(REAL-NS 1) holds (J * R) * I is REST :: thesis: for L being LinearOperator of (REAL-NS 1),(REAL-NS 1) holds (J * L) * I is LINEAR

proof

let R be REST of (REAL-NS 1),(REAL-NS 1); :: thesis: (J * R) * I is REST
A2: 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 A2;
reconsider R1 = (J * R) * I as PartFunc of REAL ,REAL ;
A3: (J * R0) * I is Function of REAL ,REAL ;
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 & abs z1 < d holds
((abs z1) " ) * (abs (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 & abs z1 < d holds
((abs z1) " ) * (abs (R1 . z1)) < r ) ) )
assume r > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) " ) * (abs (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:26;
take d ; :: thesis: ( d > 0 & ( for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) " ) * (abs (R1 . z1)) < r ) )
for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) " ) * (abs (R1 . z1)) < r

proof

let z1 be Real; :: thesis: ( z1 <> 0 & abs z1 < d implies ((abs z1) " ) * (abs (R1 . z1)) < r )
assume A8: ( z1 <> 0 & abs z1 < d ) ; :: thesis: ((abs z1) " ) * (abs (R1 . z1)) < r
reconsider z = I . z1 as Point of (REAL-NS 1) by REAL_NS1:def 4;
A9: ||.z.|| < d by A1, A8, Th3;
z1 in REAL ;
then reconsider z1r = z1 as R_eal by NUMBERS:31;
0 < |.z1r.| by A8, EXTREAL2:52;
then abs z1 > 0 by EXTREAL2:49;
then ||.z.|| <> 0 by A1, Th3;
then A10: z <> 0. (REAL-NS 1) by NORMSP_1:def 2;
A11: ||.z.|| " = (abs z1) " by A1, Th3;
R is total by NDIFF_1:def 5;
then A12: dom R = the carrier of (REAL-NS 1) by PARTFUN1:def 4;
A13: dom J = REAL 1 by FUNCT_2:def 1;
I * J = id (dom (proj 1,1)) by A1, FUNCT_1:61;
then A14: I * J = id (REAL 1) by FUNCT_2:def 1;
A15: dom (J * R0) = REAL 1 by FUNCT_2:def 1;
R /. z = R . z by A12, PARTFUN1:def 8;
then R /. z = ((id the carrier of (REAL-NS 1)) * R) . (I . z1) by FUNCT_2:23;
then R /. z = ((I * J) * R) . (I . z1) by A14, REAL_NS1:def 4;
then R /. z = (I * J) . (R . (I . z1)) by A12, FUNCT_1:23;
then R /. z = I . (J . (R0 . z)) by A13, FUNCT_1:23, FUNCT_2:7;
then R /. z = I . ((J * R0) . (I . z1)) by A15, FUNCT_1:22;
then R /. z = I . (R1 . z1) by A4, FUNCT_1:22;
then ||.(R /. z).|| = abs (R1 . z1) by A1, Th3;
hence ((abs z1) " ) * (abs (R1 . z1)) < r by A7, A9, A10, A11; :: thesis: verum

end;

hence ( d > 0 & ( for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) " ) * (abs (R1 . z1)) < r ) ) by A6; :: thesis: verum

end;

for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 )

proof

let h be convergent_to_0 Real_Sequence; :: thesis: ( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 )

A16: now

let r0 be real number ; :: thesis: ( r0 > 0 implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((((h " ) (#) (R1 /* h)) . n) - 0 ) < r0 )
reconsider r = r0 as Real by XREAL_0:def 1;
assume r0 > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs ((((h " ) (#) (R1 /* h)) . n) - 0 ) < r0
then consider d being Real such that
A17: d > 0 and
A18: for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) " ) * (abs (R1 . z1)) < r by A5;
reconsider d1 = d as real number ;
( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
then consider m being Element of NAT such that
A19: for n being Element of NAT st m <= n holds
abs ((h . n) - 0 ) < d1 by A17, SEQ_2:def 7;
take m = m; :: thesis: for n being Element of NAT st m <= n holds
abs ((((h " ) (#) (R1 /* h)) . n) - 0 ) < r0

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( m <= n implies abs ((((h " ) (#) (R1 /* h)) . n) - 0 ) < r0 )
assume m <= n ; :: thesis: abs ((((h " ) (#) (R1 /* h)) . n) - 0 ) < r0
then A20: abs ((h . n) - 0 ) < d by A19;
h is non-zero by FDIFF_1:def 1;
then A21: h . n <> 0 by SEQ_1:7;
rng h c= dom R1 by A4;
then ((abs (h . n)) " ) * (abs (R1 . (h . n))) = ((abs (h . n)) " ) * (abs ((R1 /* h) . n)) by FUNCT_2:185
.= (((abs h) . n) " ) * (abs ((R1 /* h) . n)) by SEQ_1:16
.= (((abs h) " ) . n) * (abs ((R1 /* h) . n)) by VALUED_1:10
.= ((abs (h " )) . n) * (abs ((R1 /* h) . n)) by SEQ_1:62
.= (abs ((h " ) . n)) * (abs ((R1 /* h) . n)) by SEQ_1:16
.= abs (((h " ) . n) * ((R1 /* h) . n)) by COMPLEX1:151
.= abs ((((h " ) (#) (R1 /* h)) . n) - 0 ) by SEQ_1:12 ;
hence abs ((((h " ) (#) (R1 /* h)) . n) - 0 ) < r0 by A18, A20, A21; :: 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 A16, SEQ_2:def 7; :: thesis: verum

end;

hence (J * R) * I is REST by A3, FDIFF_1:def 3; :: thesis: verum

end;

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

proof

let L be LinearOperator of (REAL-NS 1),(REAL-NS 1); :: thesis: (J * L) * I is LINEAR
A22: 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 ;
A23: ( dom L0 = REAL 1 & dom (J * L0) = REAL 1 & dom ((J * L0) * I) = REAL ) by FUNCT_2:def 1;
consider r being Real such that
A24: r = L1 . 1 ;
for p being Real holds L1 . p = r * p

proof

let p be Real; :: thesis: L1 . p = r * p
reconsider 1p = I . 1 as VECTOR of (REAL-NS 1) by REAL_NS1:def 4;
dom I = REAL by FUNCT_2:def 1;
then L1 . p = (J * L) . (I . (p * 1)) by FUNCT_1:23;
then L1 . p = (J * L) . (p * 1p) by A1, Th3;
then L1 . p = J . (L . (p * 1p)) by A22, A23, FUNCT_1:23;
then L1 . p = J . (p * (L . 1p)) by LOPBAN_1:def 6;
then L1 . p = p * (J . (L . 1p)) by A1, Th4;
then L1 . p = p * ((J * L0) . (I . 1)) by A23, FUNCT_1:22;
hence L1 . p = r * p by A23, A24, FUNCT_1:22; :: thesis: verum

end;

hence (J * L) * I is LINEAR by FDIFF_1:def 4; :: thesis: verum

end;