let S, T, U be RealNormSpace; :: thesis: for R1 being RestFunc of S,T st R1 /. (0. S) = 0. T holds
for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is RestFunc of S,U
let R1 be RestFunc of S,T; :: thesis: ( R1 /. (0. S) = 0. T implies for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is RestFunc of S,U )
assume A1: R1 /. (0. S) = 0. T ; :: thesis: for R2 being RestFunc of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is RestFunc of S,U
let R2 be RestFunc of T,U; :: thesis: ( R2 /. (0. T) = 0. U implies R2 * R1 is RestFunc of S,U )
assume A2: R2 /. (0. T) = 0. U ; :: thesis: R2 * R1 is RestFunc of S,U
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of T by PARTFUN1:def 2;
then A3: rng R1 c= dom R2 ;
A4: R1 is total by NDIFF_1:def 5;
then A5: dom R1 = the carrier of S by PARTFUN1:def 2;
A6: now :: thesis: for e0 being Real st e0 > 0 holds
ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 ) )
consider d1 being Real such that
A7: 0 < d1 and
A8: for h being Point of S st ||.h.|| < d1 holds
||.(R1 /. h).|| <= 1 * ||.h.|| by A1, Th7;
let e0 be Real; :: thesis: ( e0 > 0 implies ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 ) ) )
assume A9: e0 > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 ) )
set e = e0 / 2;
A10: e0 / 2 < e0 by A9, XREAL_1:216;
e0 / 2 > 0 by A9, XREAL_1:215;
then consider d2 being Real such that
A11: 0 < d2 and
A12: for z being Point of T st ||.z.|| < d2 holds
||.(R2 /. z).|| <= (e0 / 2) * ||.z.|| by A2, Th7;
set d = min (d1,d2);
A13: min (d1,d2) <= d2 by XXREAL_0:17;
A14: min (d1,d2) <= d1 by XXREAL_0:17;
A15: now :: thesis: for h being Point of S st h <> 0. S & ||.h.|| < min (d1,d2) holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0
let h be Point of S; :: thesis: ( h <> 0. S & ||.h.|| < min (d1,d2) implies (||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 )
assume that
A16: h <> 0. S and
A17: ||.h.|| < min (d1,d2) ; :: thesis: (||.h.|| ") * ||.((R2 * R1) /. h).|| < e0
||.h.|| < d1 by A14, A17, XXREAL_0:2;
then A18: ||.(R1 /. h).|| <= 1 * ||.h.|| by A8;
then ||.(R1 /. h).|| < min (d1,d2) by A17, XXREAL_0:2;
then ||.(R1 /. h).|| < d2 by A13, XXREAL_0:2;
then A19: ||.(R2 /. (R1 /. h)).|| <= (e0 / 2) * ||.(R1 /. h).|| by A12;
(e0 / 2) * ||.(R1 /. h).|| <= (e0 / 2) * ||.h.|| by A9, A18, XREAL_1:64;
then A20: ||.(R2 /. (R1 /. h)).|| <= (e0 / 2) * ||.h.|| by A19, XXREAL_0:2;
A21: ||.h.|| <> 0 by A16, NORMSP_0:def 5;
then ||.h.|| > 0 by NORMSP_1:4;
then (||.h.|| ") * ||.(R2 /. (R1 /. h)).|| <= (||.h.|| ") * ((e0 / 2) * ||.h.||) by A20, XREAL_1:64;
then (||.h.|| ") * ||.(R2 /. (R1 /. h)).|| <= ((||.h.|| ") * ||.h.||) * (e0 / 2) ;
then A22: (||.h.|| ") * ||.(R2 /. (R1 /. h)).|| <= 1 * (e0 / 2) by A21, XCMPLX_0:def 7;
R2 /. (R1 /. h) = (R2 * R1) /. h by A5, A3, PARTFUN2:5;
hence (||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 by A10, A22, XXREAL_0:2; :: thesis: verum
end;
0 < min (d1,d2) by A11, A7, XXREAL_0:15;
hence ex d being Real st
( d > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < d holds
(||.h.|| ") * ||.((R2 * R1) /. h).|| < e0 ) ) by A15; :: thesis: verum
end;
dom (R2 * R1) = dom R1 by A3, RELAT_1:27
.= the carrier of S by A4, PARTFUN1:def 2 ;
then R2 * R1 is total by PARTFUN1:def 2;
hence R2 * R1 is RestFunc of S,U by A6, NDIFF_1:23; :: thesis: verum