A1: {} REAL is closed by XBOOLE_1:3;
( ([#] REAL) ` = {} REAL & REAL c= REAL & [#] REAL = REAL ) by XBOOLE_1:37;
then reconsider Z = [#] REAL as open Subset of REAL by A1, RCOMP_1:def 5;
reconsider cf = REAL --> (In (0,REAL)) as Function of REAL,REAL ;
set R = cf;
reconsider f = cf as PartFunc of REAL,REAL ;

let n be Nat; :: thesis:
A4: rng h c= dom cf ;
A6: n in NAT by ORDINAL1:def 12;
thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by SEQ_1:8
.= ((h ") . n) * (cf . (h . n)) by A6, A4, FUNCT_2:108
.= ((h ") . n) * 0
.= 0 ; :: thesis:

end;

end;

then reconsider R = cf as RestFunc by Def2;
set L = cf;
for p being Real holds cf . p = 0 * p ;
then reconsider L = cf as LinearFunc by Def3;
f | Z is constant ;
then consider r being Element of REAL such that
A8: for x being Element of REAL st x in Z /\ (dom f) holds
f . x = r by PARTFUN2:57;

let x0 be Real; :: thesis:
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
assume x0 in Z ; :: thesis:
set N = the Neighbourhood of x0;
A11: xx0 in Z /\ (dom f) ;
for x being Real st x in the Neighbourhood of x0 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

let x be Real; :: thesis:
reconsider xx = x as Element of REAL by XREAL_0:def 1;
assume x in the Neighbourhood of x0 ; :: thesis:
then x in Z /\ (dom f) ;
hence (f . x) - (f . x0) = r - (f . x0) by A8
.= r - r by A8, A11
.= (L . (xx - xx0)) + 0
.= (L . (x - x0)) + (R . (x - x0)) ;
:: thesis:

end;

end;

set x0 = the Element of REAL ;
f is_differentiable_in the Element of REAL by A9;
then consider N being Neighbourhood of the Element of REAL such that
N c= dom f and
A12: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
(f . x) - (f . the Element of REAL ) = (L . (x - the Element of REAL )) + (R . (x - the Element of REAL )) ;
consider L being LinearFunc, R being RestFunc such that
A13: for x being Real st x in N holds
(f . x) - (f . the Element of REAL ) = (L . (x - the Element of REAL )) + (R . (x - the Element of REAL )) by A12;
take R ; :: thesis:
consider p being Real such that
A14: for r being Real holds L . r = p * r by Def3;
(f . the Element of REAL ) - (f . the Element of REAL ) = (L . ( the Element of REAL - the Element of REAL )) + (R . ( the Element of REAL - the Element of REAL )) by A13, RCOMP_1:16;
then A15: 0 = (p * 0) + (R . 0) by A14;
hence R . 0 = 0 ; :: thesis:

let n be Nat; :: thesis:
|.(((h ") (#) (R /* h)) . n).| = |.(((h ") . n) * ((R /* h) . n)).| by SEQ_1:8
.= |.(((h . n) ") * ((R /* h) . n)).| by VALUED_1:10 ;
then A20: |.(((h . n) ") * ((R /* h) . n)).| <= M by A18;
0 <= |.((R /* h) . n).| by COMPLEX1:46;
then 0 <= (abs (R /* h)) . n by SEQ_1:12;
hence (seq_const 0) . n <= (abs (R /* h)) . n ; :: thesis:
|.(h . n).| >= 0 by COMPLEX1:46;
then |.(h . n).| * |.(((h . n) ") * ((R /* h) . n)).| <= M * |.(h . n).| by A20, XREAL_1:64;
then |.((h . n) * (((h . n) ") * ((R /* h) . n))).| <= M * |.(h . n).| by COMPLEX1:65;
then A21: |.(((h . n) * ((h . n) ")) * ((R /* h) . n)).| <= M * |.(h . n).| ;
h . n <> 0 by SEQ_1:5;
then |.(1 * ((R /* h) . n)).| <= M * |.(h . n).| by A21, XCMPLX_0:def 7;
then |.((R /* h) . n).| <= M * ((abs h) . n) by SEQ_1:12;
then |.((R /* h) . n).| <= (M (#) (abs h)) . n by SEQ_1:9;
hence (abs (R /* h)) . n <= (M (#) (abs h)) . n by SEQ_1:12; :: thesis:

end;

end;

end;