let n, m be non zero Element of NAT ; :: thesis: for R being RestFunc of ()
for L being Lipschitzian LinearOperator of (),() holds L * R is RestFunc of ()

let R be RestFunc of (); :: thesis: for L being Lipschitzian LinearOperator of (),() holds L * R is RestFunc of ()
let L be Lipschitzian LinearOperator of (),(); :: thesis: L * R is RestFunc of ()
set S = REAL-NS n;
set T = REAL-NS m;
consider K being Real such that
A1: 0 <= K and
A2: for z being Point of () holds ||.(L . z).|| <= K * by LOPBAN_1:def 8;
dom L = the carrier of () 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;
reconsider p0 = 0 , p1 = 1 as Real ;
A6: p0 + K < p1 + K by XREAL_1:8;
now :: thesis: for ee being Real st ee > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
() * ||.((L * R) /. h).|| < ee ) )
let ee be Real; :: thesis: ( ee > 0 implies ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
() * ||.((L * R) /. h).|| < ee ) ) )

assume A7: ee > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
() * ||.((L * R) /. h).|| < ee ) )

set e = ee / 2;
ee / 2 > 0 by ;
then A8: 0 / (1 + K) < (ee / 2) / (1 + K) by ;
set e1 = (ee / 2) / (1 + K);
consider d being Real such that
A9: 0 < d and
A10: for h being Real st h <> 0 & |.h.| < d holds
() * ||.(R /. h).|| < (ee / 2) / (1 + K) by A4, A8, Th23;
A11: ee / 2 < ee by ;
now :: thesis: for h being Real st h <> 0 & |.h.| < d holds
() * ||.((L * R) /. h).|| < ee
let h be Real; :: thesis: ( h <> 0 & |.h.| < d implies () * ||.((L * R) /. h).|| < ee )
assume that
A12: h <> 0 and
A13: |.h.| < d ; :: thesis: () * ||.((L * R) /. h).|| < ee
reconsider hh = h as Element of REAL by XREAL_0:def 1;
(|.h.| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by ;
then (K + 1) * (() * ||.(R /. h).||) <= (K + 1) * ((ee / 2) / (1 + K)) by ;
then A14: (K + 1) * (() * ||.(R /. h).||) <= ee / 2 by ;
|.h.| <> 0 by ;
then A15: |.h.| > 0 by COMPLEX1:46;
A16: K * ||.(R /. h).|| <= (K + 1) * ||.(R /. h).|| by ;
||.(L /. (R /. h)).|| <= K * ||.(R /. h).|| by A2;
then ||.(L /. (R /. h)).|| <= (K + 1) * ||.(R /. h).|| by ;
then (|.h.| ") * ||.(L /. (R /. h)).|| <= () * ((K + 1) * ||.(R /. h).||) by ;
then A17: (|.h.| ") * ||.(L /. (R /. h)).|| <= ee / 2 by ;
L /. (R /. h) = L /. (R /. hh)
.= (L * R) /. hh by ;
hence (|.h.| ") * ||.((L * R) /. h).|| < ee by ; :: thesis: verum
end;
hence ex d being Real st
( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds
() * ||.((L * R) /. h).|| < ee ) ) by A9; :: thesis: verum
end;
hence L * R is RestFunc of () by ; :: thesis: verum