let S be RealNormSpace; :: thesis: for R being RestFunc of S st R /. 0 = 0. S holds
for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) )
let R be RestFunc of S; :: thesis: ( R /. 0 = 0. S implies for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) ) )
assume A1: R /. 0 = 0. S ; :: thesis: for e being Real st e > 0 holds
ex d being Real st
( d > 0 & ( for h being Real 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 Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) ) )
assume A2: e > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) )
R is total by NDIFF_3:def 1;
then consider d being Real such that
A3: d > 0 and
A4: for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * ||.(R /. z).|| < e by A2, Th1;
take d ; :: thesis: ( d > 0 & ( for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.| ) )

now :: thesis: for h being Real st |.h.| < d holds
||.(R /. h).|| <= e * |.h.|

let h be Real; :: thesis: ( |.h.| < d implies ||.(R /. b₁).|| <= e * |.b₁.| )
assume A5: |.h.| < d ; :: thesis: ||.(R /. b₁).|| <= e * |.b₁.|
A6: 0 <= |.h.| by COMPLEX1:46;

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

suppose A7: h <> 0 ; :: thesis: ||.(R /. b₁).|| <= e * |.b₁.|

then (|.h.| ") * ||.(R /. h).|| <= e by A4, A5;
then |.h.| * ((|.h.| ") * ||.(R /. h).||) <= |.h.| * e by A6, XREAL_1:64;
then A8: (|.h.| * (|.h.| ")) * ||.(R /. h).|| <= e * |.h.| ;
|.h.| <> 0 by A7, COMPLEX1:45;
then 1 * ||.(R /. h).|| <= e * |.h.| by A8, XCMPLX_0:def 7;
hence ||.(R /. h).|| <= e * |.h.| ; :: thesis: verum

end;

suppose A9: h = 0 ; :: thesis: ||.(R /. b₁).|| <= e * |.b₁.|

reconsider p0 = 0 as Real ;
p0 * |.h.| <= e * |.h.| by A2, A6;
hence ||.(R /. h).|| <= e * |.h.| by A1, A9; :: thesis: verum

end;

end;

end;

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