let S, T be non trivial RealNormSpace; :: thesis: for R being REST of S,T st R /. (0. S) = 0. T holds
for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) )
let R be REST of S,T; :: thesis: ( R /. (0. S) = 0. T implies for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) ) )
assume A1: R /. (0. S) = 0. T ; :: thesis: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) )
let e be Real; :: thesis: ( e > 0 implies ex d being Real st
( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) ) )
assume A2: e > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) )
R is total by NDIFF_1:def 5;
then consider d being Real such that
A3: d > 0 and
A4: for z being Point of S st z <> 0. S & ||.z.|| < d holds
(||.z.|| " ) * ||.(R /. z).|| < e by A2, NDIFF_1:26;
take d ; :: thesis: ( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) )

now

let h be Point of S; :: thesis: ( ||.h.|| < d implies ||.(R /. h).|| <= e * ||.h.|| )
assume A5: ||.h.|| < d ; :: thesis: ||.(R /. h).|| <= e * ||.h.||

now

per cases ( h <> 0. S or h = 0. S ) ;

case A6: h <> 0. S ; :: thesis: ||.(R /. h).|| <= e * ||.h.||

then ( 0 <= ||.h.|| & (||.h.|| " ) * ||.(R /. h).|| <= e ) by A4, A5, NORMSP_1:8;
then ||.h.|| * ((||.h.|| " ) * ||.(R /. h).||) <= ||.h.|| * e by XREAL_1:66;
then A7: (||.h.|| * (||.h.|| " )) * ||.(R /. h).|| <= e * ||.h.|| ;
||.h.|| <> 0 by A6, NORMSP_0:def 5;
then 1 * ||.(R /. h).|| <= e * ||.h.|| by A7, XCMPLX_0:def 7;
hence ||.(R /. h).|| <= e * ||.h.|| ; :: thesis: verum

end;

case A8: h = 0. S ; :: thesis: ||.(R /. h).|| <= e * ||.h.||

0 <= ||.h.|| by NORMSP_1:8;
then 0 * ||.h.|| <= e * ||.h.|| by A2;
hence ||.(R /. h).|| <= e * ||.h.|| by A1, A8, NORMSP_0:def 6; :: thesis: verum

end;

end;

end;

hence ||.(R /. h).|| <= e * ||.h.|| ; :: thesis: verum

end;

hence ( d > 0 & ( for h being Point of S st ||.h.|| < d holds
||.(R /. h).|| <= e * ||.h.|| ) ) by A3; :: thesis: verum