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;
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