let S, T be non trivial RealNormSpace; :: thesis: for R being REST of S
for L being bounded LinearOperator of S,T holds L * R is REST of T
let R be REST of S; :: thesis: for L being bounded LinearOperator of S,T holds L * R is REST of T
let L be bounded LinearOperator of S,T; :: thesis: L * R is REST of T
consider K being Real such that
A1: 0 <= K and
A2: for z being Point of S holds ||.(L . z).|| <= K * ||.z.|| by LOPBAN_1:def 8;
dom L = the carrier of S by FUNCT_2:def 1;
then A3: rng R c= dom L ;
A4: R is total by NDIFF_3:def 1;
then A5: dom R = REAL by PARTFUN1:def 2;

now

let e be Real; :: thesis: ( e > 0 implies ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < e ) ) )
assume A8: e > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < e ) )
set e1 = (e / 2) / (1 + K);
consider d being Real such that
A10: 0 < d and
A11: for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.(R /. h).|| < (e / 2) / (1 + K) by A1, A4, A8, NDIFF126;
A12: e / 2 < e by A8, XREAL_1:216;

now

let h be Real; :: thesis: ( h <> 0 & |.h.| < d implies (|.h.| ") * ||.((L * R) /. h).|| < e )
assume A13: ( h <> 0 & |.h.| < d ) ; :: thesis: (|.h.| ") * ||.((L * R) /. h).|| < e
then (|.h.| ") * ||.(R /. h).|| < (e / 2) / (1 + K) by A11;
then (K + 1) * ((|.h.| ") * ||.(R /. h).||) <= (K + 1) * ((e / 2) / (1 + K)) by A1, XREAL_1:64;
then A15: (K + 1) * ((|.h.| ") * ||.(R /. h).||) <= e / 2 by A1, XCMPLX_1:87;
|.h.| <> 0 by A13, COMPLEX1:45;
then A16: |.h.| > 0 by COMPLEX1:46;
reconsider p0 = 0 , p1 = 1 as Real ;
p0 + K < p1 + K by XREAL_1:8;
then A17: K * ||.(R /. h).|| <= (K + 1) * ||.(R /. h).|| by XREAL_1:64;
||.(L . (R /. h)).|| <= K * ||.(R /. h).|| by A2;
then ||.(L . (R /. h)).|| <= (K + 1) * ||.(R /. h).|| by A17, XXREAL_0:2;
then (|.h.| ") * ||.(L . (R /. h)).|| <= (|.h.| ") * ((K + 1) * ||.(R /. h).||) by A16, XREAL_1:64;
then A18: (|.h.| ") * ||.(L . (R /. h)).|| <= e / 2 by A15, XXREAL_0:2;
L . (R /. h) = L /. (R /. h) ;
then L . (R /. h) = (L * R) /. h by A5, A3, PARTFUN2:5;
hence (|.h.| ") * ||.((L * R) /. h).|| < e by A12, A18, XXREAL_0:2; :: thesis: verum

end;

hence ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
(|.h.| ") * ||.((L * R) /. h).|| < e ) ) by A10; :: thesis: verum

end;

hence L * R is REST of T by A4, NDIFF126; :: thesis: verum