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 that
A1: I = (proj (1,1)) " and
A2: 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
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 & 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
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 & 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 that
A9: z1 <> 0 and
A10: 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;
z1 in REAL ;
then reconsider z1r = z1 as R_eal by NUMBERS:31;
0 < |.z1r.| by A9, EXTREAL2:4;
then abs z1 > 0 by EXTREAL2:1;
then ||.z.|| <> 0 by A1, Th3;
then A11: z <> 0. (REAL-NS 1) by NORMSP_0:def 6;
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).|| = abs (R1 . z1) by A1, Th3;
A17: ||.z.|| " = (abs z1) " by A1, Th3;
||.z.|| < d by A1, A10, Th3;
hence ((abs z1) ") * (abs (R1 . z1)) < r by A8, A11, A17, A16; :: thesis: verum

end;

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

A18: 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;
A19: lim h = 0 by FDIFF_1: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
A20: d > 0 and
A21: for z1 being Real st z1 <> 0 & abs z1 < d holds
((abs z1) ") * (abs (R1 . z1)) < r by A6;
reconsider d1 = d as real number ;
h is convergent by FDIFF_1:def 1;
then consider m being Element of NAT such that
A22: for n being Element of NAT st m <= n holds
abs ((h . n) - 0) < d1 by A20, A19, 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 )
h is non-empty by FDIFF_1:def 1;
then A23: h . n <> 0 by SEQ_1:5;
rng h c= dom R1 by A5;
then A24: ((abs (h . n)) ") * (abs (R1 . (h . n))) = ((abs (h . n)) ") * (abs ((R1 /* h) . n)) by FUNCT_2:108
.= (((abs h) . n) ") * (abs ((R1 /* h) . n)) by SEQ_1:12
.= (((abs h) ") . n) * (abs ((R1 /* h) . n)) by VALUED_1:10
.= ((abs (h ")) . n) * (abs ((R1 /* h) . n)) by SEQ_1:54
.= (abs ((h ") . n)) * (abs ((R1 /* h) . n)) by SEQ_1:12
.= abs (((h ") . n) * ((R1 /* h) . n)) by COMPLEX1:65
.= abs ((((h ") (#) (R1 /* h)) . n) - 0) by SEQ_1:8 ;
assume m <= n ; :: thesis: abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0
then abs ((h . n) - 0) < d by A22;
hence abs ((((h ") (#) (R1 /* h)) . n) - 0) < r0 by A21, A23, A24; :: 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 REST 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 LINEAR :: thesis: verum

proof

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

proof

reconsider 1p = I . 1 as VECTOR of (REAL-NS 1) by REAL_NS1:def 4;
let p be Real; :: thesis: L1 . p = r * p
dom I = REAL by FUNCT_2:def 1;
then L1 . p = (J * L) . (I . (p * 1)) by FUNCT_1:13;
then L1 . p = (J * L) . (p * 1p) by A1, Th3;
then L1 . p = J . (L . (p * 1p)) by A25, A29, 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 . 1)) by A26, FUNCT_1:12;
hence L1 . p = r * p by A28, A27, FUNCT_1:12; :: thesis: verum

end;

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

end;