let S, T, U be non trivial RealNormSpace; :: thesis: for R1 being REST of S,T st R1 /. (0. S) = 0. T holds
for R2 being REST of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is REST of S,U
let R1 be REST of S,T; :: thesis: ( R1 /. (0. S) = 0. T implies for R2 being REST of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is REST of S,U )
assume A1: R1 /. (0. S) = 0. T ; :: thesis: for R2 being REST of T,U st R2 /. (0. T) = 0. U holds
R2 * R1 is REST of S,U
let R2 be REST of T,U; :: thesis: ( R2 /. (0. T) = 0. U implies R2 * R1 is REST of S,U )
assume A2: R2 /. (0. T) = 0. U ; :: thesis: R2 * R1 is REST of S,U
A3: R1 is total by NDIFF_1:def 5;
then A4: dom R1 = the carrier of S by PARTFUN1:def 4;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of T by PARTFUN1:def 4;
then A5: rng R1 c= dom R2 ;
then dom (R2 * R1) = dom R1 by RELAT_1:46
.= the carrier of S by A3, PARTFUN1:def 4 ;
then A6: R2 * R1 is total by PARTFUN1:def 4;

now

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 A7: 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;
A8: e0 / 2 > 0 by A7, XREAL_1:217;
A9: e0 / 2 < e0 by A7, XREAL_1:218;
consider d2 being Real such that
A10: 0 < d2 and
A11: for z being Point of T st ||.z.|| < d2 holds
||.(R2 /. z).|| <= (e0 / 2) * ||.z.|| by A2, A8, Th7;
consider d1 being Real such that
A12: 0 < d1 and
A13: for h being Point of S st ||.h.|| < d1 holds
||.(R1 /. h).|| <= 1 * ||.h.|| by A1, Th7;
set d = min d1,d2;
A14: ( min d1,d2 <= d1 & min d1,d2 <= d2 ) by XXREAL_0:17;
A15: 0 < min d1,d2 by A10, A12, XXREAL_0:15;

now

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
A18: R2 /. (R1 /. h) = (R2 * R1) /. h by A4, A5, PARTFUN2:10;
||.h.|| < d1 by A14, A17, XXREAL_0:2;
then A19: ||.(R1 /. h).|| <= 1 * ||.h.|| by A13;
then ||.(R1 /. h).|| < min d1,d2 by A17, XXREAL_0:2;
then ||.(R1 /. h).|| < d2 by A14, XXREAL_0:2;
then A20: ||.(R2 /. (R1 /. h)).|| <= (e0 / 2) * ||.(R1 /. h).|| by A11;
(e0 / 2) * ||.(R1 /. h).|| <= (e0 / 2) * ||.h.|| by A8, A19, XREAL_1:66;
then A21: ||.(R2 /. (R1 /. h)).|| <= (e0 / 2) * ||.h.|| by A20, XXREAL_0:2;
A22: ||.h.|| <> 0 by A16, NORMSP_1:def 2;
then ||.h.|| > 0 by NORMSP_1:8;
then ||.h.|| " > 0 ;
then (||.h.|| " ) * ||.(R2 /. (R1 /. h)).|| <= (||.h.|| " ) * ((e0 / 2) * ||.h.||) by A21, XREAL_1:66;
then (||.h.|| " ) * ||.(R2 /. (R1 /. h)).|| <= ((||.h.|| " ) * ||.h.||) * (e0 / 2) ;
then (||.h.|| " ) * ||.(R2 /. (R1 /. h)).|| <= 1 * (e0 / 2) by A22, XCMPLX_0:def 7;
hence (||.h.|| " ) * ||.((R2 * R1) /. h).|| < e0 by A9, A18, XXREAL_0:2; :: thesis: verum

end;

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;

hence R2 * R1 is REST of S,U by A6, NDIFF_1:26; :: thesis: verum