let n, m be non zero Element of NAT ; :: thesis: for R being RestFunc of (REAL-NS n)

for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m)

let R be RestFunc of (REAL-NS n); :: thesis: for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m)

let L be Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m); :: thesis: L * R is RestFunc of (REAL-NS m)

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 (REAL-NS n) holds ||.(L . z).|| <= K * ||.z.|| by LOPBAN_1:def 8;

dom L = the carrier of (REAL-NS n) 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;

for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m)

let R be RestFunc of (REAL-NS n); :: thesis: for L being Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) holds L * R is RestFunc of (REAL-NS m)

let L be Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m); :: thesis: L * R is RestFunc of (REAL-NS m)

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 (REAL-NS n) holds ||.(L . z).|| <= K * ||.z.|| by LOPBAN_1:def 8;

dom L = the carrier of (REAL-NS n) 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

(|.h.| ") * ||.((L * R) /. h).|| < ee ) )

hence
L * R is RestFunc of (REAL-NS m)
by A4, Th23; :: thesis: verumex d being Real st

( d > 0 & ( for h being Real st h <> 0 & |.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 Real st h <> 0 & |.h.| < d holds

(|.h.| ") * ||.((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

(|.h.| ") * ||.((L * R) /. h).|| < ee ) )

set e = ee / 2;

ee / 2 > 0 by A7, XREAL_1:215;

then A8: 0 / (1 + K) < (ee / 2) / (1 + K) by A1, XREAL_1:74;

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

(|.h.| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by A4, A8, Th23;

A11: ee / 2 < ee by A7, XREAL_1:216;

( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds

(|.h.| ") * ||.((L * R) /. h).|| < ee ) ) by A9; :: thesis: verum

end;( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds

(|.h.| ") * ||.((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

(|.h.| ") * ||.((L * R) /. h).|| < ee ) )

set e = ee / 2;

ee / 2 > 0 by A7, XREAL_1:215;

then A8: 0 / (1 + K) < (ee / 2) / (1 + K) by A1, XREAL_1:74;

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

(|.h.| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by A4, A8, Th23;

A11: ee / 2 < ee by A7, XREAL_1:216;

now :: thesis: for h being Real st h <> 0 & |.h.| < d holds

(|.h.| ") * ||.((L * R) /. h).|| < ee

hence
ex d being Real st (|.h.| ") * ||.((L * R) /. h).|| < ee

let h be Real; :: thesis: ( h <> 0 & |.h.| < d implies (|.h.| ") * ||.((L * R) /. h).|| < ee )

assume that

A12: h <> 0 and

A13: |.h.| < d ; :: thesis: (|.h.| ") * ||.((L * R) /. h).|| < ee

reconsider hh = h as Element of REAL by XREAL_0:def 1;

(|.h.| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by A10, A12, A13;

then (K + 1) * ((|.h.| ") * ||.(R /. h).||) <= (K + 1) * ((ee / 2) / (1 + K)) by A1, XREAL_1:64;

then A14: (K + 1) * ((|.h.| ") * ||.(R /. h).||) <= ee / 2 by A1, XCMPLX_1:87;

|.h.| <> 0 by A12, COMPLEX1:45;

then A15: |.h.| > 0 by COMPLEX1:46;

A16: 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 A16, XXREAL_0:2;

then (|.h.| ") * ||.(L /. (R /. h)).|| <= (|.h.| ") * ((K + 1) * ||.(R /. h).||) by A15, XREAL_1:64;

then A17: (|.h.| ") * ||.(L /. (R /. h)).|| <= ee / 2 by A14, XXREAL_0:2;

L /. (R /. h) = L /. (R /. hh)

.= (L * R) /. hh by A5, A3, PARTFUN2:5 ;

hence (|.h.| ") * ||.((L * R) /. h).|| < ee by A11, A17, XXREAL_0:2; :: thesis: verum

end;assume that

A12: h <> 0 and

A13: |.h.| < d ; :: thesis: (|.h.| ") * ||.((L * R) /. h).|| < ee

reconsider hh = h as Element of REAL by XREAL_0:def 1;

(|.h.| ") * ||.(R /. h).|| < (ee / 2) / (1 + K) by A10, A12, A13;

then (K + 1) * ((|.h.| ") * ||.(R /. h).||) <= (K + 1) * ((ee / 2) / (1 + K)) by A1, XREAL_1:64;

then A14: (K + 1) * ((|.h.| ") * ||.(R /. h).||) <= ee / 2 by A1, XCMPLX_1:87;

|.h.| <> 0 by A12, COMPLEX1:45;

then A15: |.h.| > 0 by COMPLEX1:46;

A16: 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 A16, XXREAL_0:2;

then (|.h.| ") * ||.(L /. (R /. h)).|| <= (|.h.| ") * ((K + 1) * ||.(R /. h).||) by A15, XREAL_1:64;

then A17: (|.h.| ") * ||.(L /. (R /. h)).|| <= ee / 2 by A14, XXREAL_0:2;

L /. (R /. h) = L /. (R /. hh)

.= (L * R) /. hh by A5, A3, PARTFUN2:5 ;

hence (|.h.| ") * ||.((L * R) /. h).|| < ee by A11, A17, XXREAL_0:2; :: thesis: verum

( d > 0 & ( for h being Real st h <> 0 & |.h.| < d holds

(|.h.| ") * ||.((L * R) /. h).|| < ee ) ) by A9; :: thesis: verum