let n be non zero Element of NAT ; :: thesis: for R being RestFunc of () st R /. 0 = 0. () 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 (); :: thesis: ( R /. 0 = 0. () 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. () ; :: 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
() * ||.(R /. z).|| < e by ;
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.| & () * ||.(R /. h).|| <= e ) by ;
then |.h.| * (() * ||.(R /. h).||) <= |.h.| * e by XREAL_1:64;
then A7: (|.h.| * ()) * ||.(R /. h).|| <= e * |.h.| ;
|.h.| <> 0 by ;
then 1 * ||.(R /. h).|| <= e * |.h.| by ;
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