let n be non zero Element of NAT ; :: thesis: for R being RestFunc of (REAL-NS n) st R /. 0 = 0. (REAL-NS n) 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 (REAL-NS n); :: thesis: ( R /. 0 = 0. (REAL-NS n) 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. (REAL-NS n) ; :: 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, Th23;
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 /. h).|| <= e * |.h.| )
assume A5: |.h.| < d ; :: thesis: ||.(R /. h).|| <= e * |.h.|

now :: thesis: ( ( h <> 0 & ||.(R /. h).|| <= e * |.h.| ) or ( h = 0 & ||.(R /. h).|| <= e * |.h.| ) )

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

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

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

end;

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

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

end;

end;

end;

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

end;

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