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.| ) )

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

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.|

hence
( d > 0 & ( 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.|

end;assume A5: |.h.| < d ; :: thesis: ||.(R /. h).|| <= e * |.h.|

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

hence
||.(R /. h).|| <= e * |.h.|
; :: thesis: verumper cases
( h <> 0 or h = 0 )
;

end;

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;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

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