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

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

let e be Real; :: thesis: ( e > 0 implies ex d1 being Real st
( d1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d1 holds
(||.h.|| ") * ||.((R * L) /. h).|| < e ) ) )
assume e > 0 ; :: thesis: ex d1 being Real st
( d1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d1 holds
(||.h.|| ") * ||.((R * L) /. h).|| < e ) )
then A8: 0 / (1 + K) < e / (1 + K) by A2, XREAL_1:74;
set e1 = e / (1 + K);
consider d being Real such that
A9: 0 < d and
A10: for h being Point of T st ||.h.|| < d holds
||.(R /. h).|| <= (e / (1 + K)) * ||.h.|| by A1, A8, Th7;
set d1 = d / (1 + K);

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

let h be Point of S; :: thesis: ( h <> 0. S & ||.h.|| < d / (1 + K) implies (||.h.|| ") * ||.((R * L) /. h).|| < e )
assume that
A12: h <> 0. S and
A13: ||.h.|| < d / (1 + K) ; :: thesis: (||.h.|| ") * ||.((R * L) /. h).|| < e
A14: ||.(L . h).|| <= K * ||.h.|| by A3;
A15: ||.h.|| <> 0 by A12, NORMSP_0:def 5;
then A16: ||.h.|| > 0 by NORMSP_1:4;
then K * ||.h.|| < (K + 1) * ||.h.|| by A6, XREAL_1:68;
then A17: ||.(L . h).|| < (K + 1) * ||.h.|| by A14, XXREAL_0:2;
(K + 1) * ||.h.|| < (K + 1) * (d / (1 + K)) by A2, A13, XREAL_1:68;
then ||.(L . h).|| < (K + 1) * (d / (1 + K)) by A17, XXREAL_0:2;
then ||.(L . h).|| < d by A2, XCMPLX_1:87;
then A18: ||.(R /. (L . h)).|| <= (e / (1 + K)) * ||.(L . h).|| by A10;
A19: R /. (L . h) = R /. (L /. h)
.= (R * L) /. h by A4, A5, PARTFUN2:5 ;
(e / (1 + K)) * ||.(L . h).|| < (e / (1 + K)) * ((K + 1) * ||.h.||) by A8, A17, XREAL_1:68;
then ||.(R /. (L . h)).|| < (e / (1 + K)) * ((K + 1) * ||.h.||) by A18, XXREAL_0:2;
then (||.h.|| ") * ||.((R * L) /. h).|| < (||.h.|| ") * (((e / (1 + K)) * (K + 1)) * ||.h.||) by A19, A16, XREAL_1:68;
then (||.h.|| ") * ||.((R * L) /. h).|| < ((||.h.|| * (||.h.|| ")) * (e / (1 + K))) * (K + 1) ;
then (||.h.|| ") * ||.((R * L) /. h).|| < (1 * (e / (1 + K))) * (K + 1) by A15, XCMPLX_0:def 7;
hence (||.h.|| ") * ||.((R * L) /. h).|| < e by A2, XCMPLX_1:87; :: thesis: verum

end;

0 / (1 + K) < d / (1 + K) by A2, A9, XREAL_1:74;
hence ex d1 being Real st
( d1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d1 holds
(||.h.|| ") * ||.((R * L) /. h).|| < e ) ) by A11; :: thesis: verum

end;

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