let I be Function of REAL ,(REAL 1); :: thesis:
let J be Function of (REAL 1),REAL ; :: thesis:
assume A1: ( I = (proj 1,1) " & J = proj 1,1 ) ; :: thesis:
thus for R being REST holds (I * R) * J is REST of (REAL-NS 1),(REAL-NS 1) :: thesis:

proof

let R be REST; :: thesis:
R is total by FDIFF_1:def 3;
then reconsider R0 = R as Function of REAL ,REAL ;
A2: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
then reconsider R1 = (I * R0) * J as PartFunc of (REAL-NS 1),(REAL-NS 1) ;
for h being convergent_to_0 sequence of (REAL-NS 1) holds
( (||.h.|| " ) (#) (R1 /* h) is convergent & lim ((||.h.|| " ) (#) (R1 /* h)) = 0. (REAL-NS 1) )

proof

let h be convergent_to_0 sequence of (REAL-NS 1); :: thesis:
A3: h is non-zero by NDIFF_1:def 4;
A4: ( h is convergent & lim h = 0. (REAL-NS 1) ) by NDIFF_1:def 4;
deffunc H₁( Element of NAT ) -> Element of REAL = J . (h . $1);
consider s being Real_Sequence such that
A5: for n being Element of NAT holds s . n = H₁(n) from SEQ_1:sch 1();
s is convergent_to_0 Real_Sequence

proof

now

let x be set ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider n = x as Element of NAT ;
h . n <> 0. (REAL-NS 1) by A3, NDIFF_1:6;
then A6: ||.(h . n).|| <> 0 by NORMSP_1:def 2;
s . n = J . (h . n) by A5;
then A7: abs (s . n) <> 0 by A1, A6, Th4;
0 <= abs (s . n) by COMPLEX1:132;
hence s . x <> 0 by A7, COMPLEX1:133; :: thesis:

end;

then A8: s is non-zero by SEQ_1:6;

A9: now

let p be real number ; :: thesis:
assume A10: 0 < p ; :: thesis:
p is Real by XREAL_0:def 1;
then consider m being Element of NAT such that
A11: for n being Element of NAT st m <= n holds
||.((h . n) - (0. (REAL-NS 1))).|| < p by A4, A10, NORMSP_1:def 11;
take m = m; :: thesis:

now

let n be Element of NAT ; :: thesis:
assume m <= n ; :: thesis:
then ||.((h . n) - (0. (REAL-NS 1))).|| < p by A11;
then A12: ||.(h . n).|| < p by RLVECT_1:26;
s . n = J . (h . n) by A5;
hence abs ((s . n) - 0 ) < p by A1, A12, Th4; :: thesis:

end;

hence for n being Element of NAT st m <= n holds
abs ((s . n) - 0 ) < p ; :: thesis:

end;

then A13: s is convergent by SEQ_2:def 6;
then lim s = 0 by A9, SEQ_2:def 7;
hence s is convergent_to_0 Real_Sequence by A8, A13, FDIFF_1:def 1; :: thesis:

end;

then reconsider s = s as convergent_to_0 Real_Sequence ;
A14: J * I = id REAL by A1, Lm1, FUNCT_1:61;

now

let n be Element of NAT ; :: thesis:
h . n in the carrier of (REAL-NS 1) ;
then A15: h . n in REAL 1 by REAL_NS1:def 4;
reconsider f1 = R1 as Function ;
A16: dom R1 = REAL 1 by FUNCT_2:def 1;
rng h c= the carrier of (REAL-NS 1) ;
then A17: rng h c= dom R1 by A16, REAL_NS1:def 4;
NAT = dom h by FUNCT_2:def 1;
then R1 . (h . n) = (f1 * h) . n by FUNCT_1:23;
then A18: R1 . (h . n) = (R1 /* h) . n by A17, FUNCT_2:def 12;
R1 is total by A2;
then (R /* s) . n = R . (s . n) by FUNCT_2:192;
then (R /* s) . n = R . (J . (h . n)) by A5;
then (R /* s) . n = (J * I) . (R0 . (J . (h . n))) by A14, FUNCT_1:35;
then (R /* s) . n = (J * I) . ((R0 * J) . (h . n)) by A15, FUNCT_2:21;
then (R /* s) . n = J . (I . ((R0 * J) . (h . n))) by FUNCT_2:21;
then (R /* s) . n = J . ((I * (R0 * J)) . (h . n)) by A15, FUNCT_2:21;
then A19: (R /* s) . n = J . ((R1 /* h) . n) by A18, RELAT_1:55;
A20: s . n = J . (h . n) by A5;
A21: ||.(h . n).|| >= 0 by NORMSP_1:8;
h . n <> 0. (REAL-NS 1) by A3, NDIFF_1:6;
then ||.(h . n).|| <> 0 by NORMSP_1:def 2;
then A22: 0 < ||.(h . n).|| " by A21;
||.((||.h.|| " ) (#) (R1 /* h)).|| . n = ||.(((||.h.|| " ) (#) (R1 /* h)) . n).|| by NORMSP_1:def 10
.= ||.(((||.h.|| " ) . n) * ((R1 /* h) . n)).|| by NDIFF_1:def 2
.= (abs ((||.h.|| " ) . n)) * ||.((R1 /* h) . n).|| by NORMSP_1:def 2
.= (abs ((||.h.|| . n) " )) * ||.((R1 /* h) . n).|| by VALUED_1:10
.= (abs (||.(h . n).|| " )) * ||.((R1 /* h) . n).|| by NORMSP_1:def 10
.= (||.(h . n).|| " ) * ||.((R1 /* h) . n).|| by A22, ABSVALUE:def 1
.= ((abs (s . n)) " ) * ||.((R1 /* h) . n).|| by A1, A20, Th4
.= ((abs (s . n)) " ) * (abs ((R /* s) . n)) by A1, A19, Th4
.= ((abs (s . n)) " ) * ((abs (R /* s)) . n) by SEQ_1:16
.= (((abs s) . n) " ) * ((abs (R /* s)) . n) by SEQ_1:16
.= (((abs s) " ) . n) * ((abs (R /* s)) . n) by VALUED_1:10
.= (((abs s) " ) (#) (abs (R /* s))) . n by SEQ_1:12
.= ((abs (s " )) (#) (abs (R /* s))) . n by SEQ_1:62 ;
hence ||.((||.h.|| " ) (#) (R1 /* h)).|| . n = (abs ((s " ) (#) (R /* s))) . n by SEQ_1:60; :: thesis:

end;

then A23: ||.((||.h.|| " ) (#) (R1 /* h)).|| = abs ((s " ) (#) (R /* s)) by FUNCT_2:113;
A24: ( (s " ) (#) (R /* s) is convergent & lim ((s " ) (#) (R /* s)) = 0 ) by FDIFF_1:def 3;
then A25: abs ((s " ) (#) (R /* s)) is convergent by SEQ_4:26;
lim (abs ((s " ) (#) (R /* s))) = abs (lim ((s " ) (#) (R /* s))) by A24, SEQ_4:27;
then A26: lim (abs ((s " ) (#) (R /* s))) = 0 by A24, ABSVALUE:7;

A27: now

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider m being Element of NAT such that
A28: for n being Element of NAT st m <= n holds
abs ((||.((||.h.|| " ) (#) (R1 /* h)).|| . n) - 0 ) < p by A23, A25, A26, SEQ_2:def 7;
take m = m; :: thesis:

hereby :: thesis:

let n be Element of NAT ; :: thesis:
assume m <= n ; :: thesis:
then abs ((||.((||.h.|| " ) (#) (R1 /* h)).|| . n) - 0 ) < p by A28;
then A29: abs ||.(((||.h.|| " ) (#) (R1 /* h)) . n).|| < p by NORMSP_1:def 10;
0 <= ||.(((||.h.|| " ) (#) (R1 /* h)) . n).|| by NORMSP_1:8;
then ||.(((||.h.|| " ) (#) (R1 /* h)) . n).|| < p by A29, ABSVALUE:def 1;
hence ||.((((||.h.|| " ) (#) (R1 /* h)) . n) - (0. (REAL-NS 1))).|| < p by RLVECT_1:26; :: thesis:

end;

then (||.h.|| " ) (#) (R1 /* h) is convergent by NORMSP_1:def 9;
hence ( (||.h.|| " ) (#) (R1 /* h) is convergent & lim ((||.h.|| " ) (#) (R1 /* h)) = 0. (REAL-NS 1) ) by A27, NORMSP_1:def 11; :: thesis:

end;

hence (I * R) * J is REST of (REAL-NS 1),(REAL-NS 1) by A2, NDIFF_1:def 5; :: thesis:

end;

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

proof

let L be LINEAR; :: thesis:
consider r being Real such that
A30: for p being Real holds L . p = r * p by FDIFF_1:def 4;
L is total by FDIFF_1:def 4;
then reconsider L0 = L as Function of REAL ,REAL ;
A31: dom L0 = REAL by FUNCT_2:def 1;
A32: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
(I * L0) * J is Function of (REAL 1),(REAL 1) ;
then reconsider L1 = (I * L) * J as Function of (REAL-NS 1),(REAL-NS 1) by A32;
A33: dom L1 = REAL 1 by A32, FUNCT_2:def 1;

A34: now

let x be VECTOR of (REAL-NS 1); :: thesis:
let a be Real; :: thesis:
I . (L . (J . x)) = (I * L) . (J . x) by A31, FUNCT_1:23;
then A35: I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:22;
L1 . (a * x) = (I * L) . (J . (a * x)) by A32, A33, FUNCT_1:22;
then L1 . (a * x) = (I * L) . (a * (J . x)) by A1, Th4;
then L1 . (a * x) = I . (L . (a * (J . x))) by A31, FUNCT_1:23;
then L1 . (a * x) = I . (r * (a * (J . x))) by A30;
then L1 . (a * x) = I . (a * (r * (J . x))) ;
then L1 . (a * x) = I . (a * (L . (J . x))) by A30;
hence L1 . (a * x) = a * (L1 . x) by A1, A35, Th3; :: thesis:

end;

now

let x, y be VECTOR of (REAL-NS 1); :: thesis:
I . (L . (J . x)) = (I * L) . (J . x) by A31, FUNCT_1:23;
then A36: I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:22;
I . (L . (J . y)) = (I * L) . (J . y) by A31, FUNCT_1:23;
then A37: I . (L . (J . y)) = L1 . y by A32, A33, FUNCT_1:22;
L1 . (x + y) = (I * L) . (J . (x + y)) by A32, A33, FUNCT_1:22;
then L1 . (x + y) = (I * L) . ((J . x) + (J . y)) by A1, Th4;
then L1 . (x + y) = I . (L . ((J . x) + (J . y))) by A31, FUNCT_1:23;
then L1 . (x + y) = I . (r * ((J . x) + (J . y))) by A30;
then L1 . (x + y) = I . ((r * (J . x)) + (r * (J . y))) ;
then L1 . (x + y) = I . ((L . (J . x)) + (r * (J . y))) by A30;
then L1 . (x + y) = I . ((L . (J . x)) + (L . (J . y))) by A30;
hence L1 . (x + y) = (L1 . x) + (L1 . y) by A1, A36, A37, Th3; :: thesis:

end;

then reconsider L1 = L1 as LinearOperator of (REAL-NS 1),(REAL-NS 1) by A34, LOPBAN_1:def 5, LOPBAN_1:def 6;
set K = abs r;
A38: 0 <= abs r by COMPLEX1:132;

now

let x be VECTOR of (REAL-NS 1); :: thesis:
I . (L . (J . x)) = (I * L) . (J . x) by A31, FUNCT_1:23;
then I . (L . (J . x)) = L1 . x by A32, A33, FUNCT_1:22;
then ||.(L1 . x).|| = abs (L . (J . x)) by A1, Th3;
then ||.(L1 . x).|| = abs (r * (J . x)) by A30;
then ||.(L1 . x).|| = (abs r) * (abs (J . x)) by COMPLEX1:151;
hence ||.(L1 . x).|| <= (abs r) * ||.x.|| by A1, Th4; :: thesis:

end;

hence (I * L) * J is bounded LinearOperator of (REAL-NS 1),(REAL-NS 1) by A38, LOPBAN_1:def 9; :: thesis:

end;