let S, T be RealNormSpace; :: thesis:
let R be RestFunc of S,T; :: thesis:
assume A1: R /. (0. S) = 0. T ; :: thesis:
let e be Real; :: thesis:
assume A2: e > 0 ; :: thesis:
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:23;
take d ; :: thesis:

let h be Point of S; :: thesis:
assume A5: ||.h.|| < d ; :: thesis:

case A6: h <> 0. S ; :: thesis:

then ( 0 <= ||.h.|| & (||.h.|| ") * ||.(R /. h).|| <= e ) by A4, A5, NORMSP_1:4;
then ||.h.|| * ((||.h.|| ") * ||.(R /. h).||) <= ||.h.|| * e by XREAL_1:64;
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:

end;

case A8: h = 0. S ; :: thesis:

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

end;

end;

end;

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

end;

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