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
for L being bounded LinearOperator of S,T holds R2 * (L + 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
for L being bounded LinearOperator of S,T holds R2 * (L + 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
for L being bounded LinearOperator of S,T holds R2 * (L + R1) is REST of S,U
let R2 be REST of T,U; :: thesis: ( R2 /. (0. T) = 0. U implies for L being bounded LinearOperator of S,T holds R2 * (L + R1) is REST of S,U )
assume A2: R2 /. (0. T) = 0. U ; :: thesis: for L being bounded LinearOperator of S,T holds R2 * (L + R1) is REST of S,U
let L be bounded LinearOperator of S,T; :: thesis: R2 * (L + R1) is REST of S,U
consider K being Real such that
A3: 0 <= K and
A4: for h being Point of S holds ||.(L . h).|| <= K * ||.h.|| by LOPBAN_1:def 9;
consider d0 being Real such that
A5: 0 < d0 and
A6: for h being Point of S st ||.h.|| < d0 holds
||.(R1 /. h).|| <= 1 * ||.h.|| by A1, Th7;
A8: R1 is total by NDIFF_1:def 5;
R2 is total by NDIFF_1:def 5;
then A9: dom R2 = the carrier of T by PARTFUN1:def 4;
A10: L + R1 is total by A8, VFUNCT_1:38;
then A11: dom (L + R1) = the carrier of S by PARTFUN1:def 4;
A12: rng (L + R1) c= dom R2 by A9;
then dom (R2 * (L + R1)) = dom (L + R1) by RELAT_1:46
.= the carrier of S by A10, PARTFUN1:def 4 ;
then A13: R2 * (L + R1) is total by PARTFUN1:def 4;

now

let ee be Real; :: thesis: ( ee > 0 implies ex dd1 being Real st
( dd1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < dd1 holds
(||.h.|| " ) * ||.((R2 * (L + R1)) /. h).|| < ee ) ) )
assume A14: ee > 0 ; :: thesis: ex dd1 being Real st
( dd1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < dd1 holds
(||.h.|| " ) * ||.((R2 * (L + R1)) /. h).|| < ee ) )
set e = ee / 2;
A15: ee / 2 > 0 by A14, XREAL_1:217;
A16: ee / 2 < ee by A14, XREAL_1:218;
set e1 = (ee / 2) / (1 + K);
A17: 0 / (1 + K) < (ee / 2) / (1 + K) by A3, A15, XREAL_1:76;
then consider d being Real such that
A18: 0 < d and
A19: for z being Point of T st ||.z.|| < d holds
||.(R2 /. z).|| <= ((ee / 2) / (1 + K)) * ||.z.|| by A2, Th7;
set d1 = d / (1 + K);
A20: 0 / (1 + K) < d / (1 + K) by A3, A18, XREAL_1:76;
set dd1 = min d0,(d / (1 + K));
A21: ( min d0,(d / (1 + K)) <= d0 & min d0,(d / (1 + K)) <= d / (1 + K) ) by XXREAL_0:17;
A22: 0 < min d0,(d / (1 + K)) by A5, A20, XXREAL_0:15;

now

let h be Point of S; :: thesis: ( h <> 0. S & ||.h.|| < min d0,(d / (1 + K)) implies (||.h.|| " ) * ||.((R2 * (L + R1)) /. h).|| < ee )
assume that
A23: h <> 0. S and
A24: ||.h.|| < min d0,(d / (1 + K)) ; :: thesis: (||.h.|| " ) * ||.((R2 * (L + R1)) /. h).|| < ee
A25: ||.h.|| < d / (1 + K) by A21, A24, XXREAL_0:2;
A26: R2 /. ((L . h) + (R1 /. h)) = R2 /. ((L /. h) + (R1 /. h))
.= R2 /. ((L + R1) /. h) by A11, VFUNCT_1:def 1
.= (R2 * (L + R1)) /. h by A11, A12, PARTFUN2:10 ;
A27: ||.h.|| <> 0 by A23, NORMSP_1:def 2;
then ||.h.|| > 0 by NORMSP_1:8;
then A28: ||.h.|| " > 0 ;
A29: ||.(L . h).|| <= K * ||.h.|| by A4;
||.h.|| < d0 by A21, A24, XXREAL_0:2;
then A30: ||.(R1 /. h).|| <= 1 * ||.h.|| by A6;
A31: ||.((L . h) + (R1 /. h)).|| <= ||.(L . h).|| + ||.(R1 /. h).|| by NORMSP_1:def 2;
||.(L . h).|| + ||.(R1 /. h).|| <= (K * ||.h.||) + (1 * ||.h.||) by A29, A30, XREAL_1:9;
then A32: ||.((L . h) + (R1 /. h)).|| <= (K + 1) * ||.h.|| by A31, XXREAL_0:2;
(K + 1) * ||.h.|| < (K + 1) * (d / (1 + K)) by A3, A25, XREAL_1:70;
then ||.((L . h) + (R1 /. h)).|| < (K + 1) * (d / (1 + K)) by A32, XXREAL_0:2;
then ||.((L . h) + (R1 /. h)).|| < d by A3, XCMPLX_1:88;
then A33: ||.(R2 /. ((L . h) + (R1 /. h))).|| <= ((ee / 2) / (1 + K)) * ||.((L . h) + (R1 /. h)).|| by A19;
((ee / 2) / (1 + K)) * ||.((L . h) + (R1 /. h)).|| <= ((ee / 2) / (1 + K)) * ((K + 1) * ||.h.||) by A17, A32, XREAL_1:66;
then ||.(R2 /. ((L . h) + (R1 /. h))).|| <= ((ee / 2) / (1 + K)) * ((K + 1) * ||.h.||) by A33, XXREAL_0:2;
then (||.h.|| " ) * ||.((R2 * (L + R1)) /. h).|| <= (||.h.|| " ) * ((((ee / 2) / (1 + K)) * (K + 1)) * ||.h.||) by A26, A28, XREAL_1:66;
then (||.h.|| " ) * ||.((R2 * (L + R1)) /. h).|| <= ((||.h.|| * (||.h.|| " )) * ((ee / 2) / (1 + K))) * (K + 1) ;
then (||.h.|| " ) * ||.((R2 * (L + R1)) /. h).|| <= (1 * ((ee / 2) / (1 + K))) * (K + 1) by A27, XCMPLX_0:def 7;
then (||.h.|| " ) * ||.((R2 * (L + R1)) /. h).|| <= ee / 2 by A3, XCMPLX_1:88;
hence (||.h.|| " ) * ||.((R2 * (L + R1)) /. h).|| < ee by A16, XXREAL_0:2; :: thesis: verum

end;

hence ex dd1 being Real st
( dd1 > 0 & ( for h being Point of S st h <> 0. S & ||.h.|| < dd1 holds
(||.h.|| " ) * ||.((R2 * (L + R1)) /. h).|| < ee ) ) by A22; :: thesis: verum

end;

hence R2 * (L + R1) is REST of S,U by A13, NDIFF_1:26; :: thesis: verum