let S, T, U be RealNormSpace; :: thesis: for R being RestFunc of S,T
for L being Lipschitzian LinearOperator of T,U holds L * R is RestFunc of S,U
let R be RestFunc of S,T; :: thesis: for L being Lipschitzian LinearOperator of T,U holds L * R is RestFunc of S,U
let L be Lipschitzian LinearOperator of T,U; :: thesis: L * R is RestFunc of S,U
consider K being Real such that
A1: 0 <= K and
A2: for z being Point of T holds ||.(L . z).|| <= K * ||.z.|| by LOPBAN_1:def 8;
dom L = the carrier of T by FUNCT_2:def 1;
then A3: rng R c= dom L ;
A4: R is total by NDIFF_1:def 5;
then A5: dom R = the carrier of S by PARTFUN1:def 2;
A6: 0 + K < 1 + K by XREAL_1:8;

A7: now :: thesis: for ee being Real st ee > 0 holds
ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((L * R) /. h).|| < ee ) )

let ee be Real; :: thesis: ( ee > 0 implies ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((L * R) /. h).|| < ee ) ) )
assume A8: ee > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((L * R) /. h).|| < ee ) )
set e = ee / 2;
ee / 2 > 0 by A8, XREAL_1:215;
then A9: 0 / (1 + K) < (ee / 2) / (1 + K) by A1, XREAL_1:74;
set e1 = (ee / 2) / (1 + K);
R is total by NDIFF_1:def 5;
then consider d being Real such that
A10: 0 < d and
A11: for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by A9, NDIFF_1:23;
A12: ee / 2 < ee by A8, XREAL_1:216;

now :: thesis: for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((L * R) /. h).|| < ee

let h be Point of S; :: thesis: ( h <> 0. S & ||.h.|| < d implies (||.h.|| ") * ||.((L * R) /. h).|| < ee )
assume that
A13: h <> 0. S and
A14: ||.h.|| < d ; :: thesis: (||.h.|| ") * ||.((L * R) /. h).|| < ee
(||.h.|| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by A11, A13, A14;
then (K + 1) * ((||.h.|| ") * ||.(R /. h).||) <= (K + 1) * ((ee / 2) / (1 + K)) by A1, XREAL_1:64;
then A15: (K + 1) * ((||.h.|| ") * ||.(R /. h).||) <= ee / 2 by A1, XCMPLX_1:87;
||.h.|| <> 0 by A13, NORMSP_0:def 5;
then A16: ||.h.|| > 0 by NORMSP_1:4;
0 <= ||.(R /. h).|| by NORMSP_1:4;
then A17: K * ||.(R /. h).|| <= (K + 1) * ||.(R /. h).|| by A6, 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)).|| <= ee / 2 by A15, XXREAL_0:2;
L . (R /. h) = L /. (R /. h)
.= (L * R) /. h by A5, A3, PARTFUN2:5 ;
hence (||.h.|| ") * ||.((L * R) /. h).|| < ee by A12, A18, XXREAL_0:2; :: thesis: verum

end;

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

end;

dom (L * R) = dom R by A3, RELAT_1:27
.= the carrier of S by A4, PARTFUN1:def 2 ;
then L * R is total by PARTFUN1:def 2;
hence L * R is RestFunc of S,U by A7, NDIFF_1:23; :: thesis: verum