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 ;

set L = cf;

for p being Real holds cf . p = 0 * p ;

then reconsider L = cf as LinearFunc by Def3;

f | Z is V8() ;

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;

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: ( R . 0 = 0 & R is_continuous_in 0 )

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: R is_continuous_in 0

( ([#] 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 ;

now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )

then reconsider R = cf as RestFunc by Def2;( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )

let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0 )

hence (h ") (#) (cf /* h) is convergent ; :: thesis: lim ((h ") (#) (cf /* h)) = 0

((h ") (#) (cf /* h)) . 0 = 0 by A3;

hence lim ((h ") (#) (cf /* h)) = 0 by A7, SEQ_4:25; :: thesis: verum

end;A3: now :: thesis: for n being Nat holds ((h ") (#) (cf /* h)) . n = 0

then A7:
(h ") (#) (cf /* h) is V8()
by VALUED_0:def 18;let n be Nat; :: thesis: ((h ") (#) (cf /* h)) . n = 0

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: verum

end;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: verum

hence (h ") (#) (cf /* h) is convergent ; :: thesis: lim ((h ") (#) (cf /* h)) = 0

((h ") (#) (cf /* h)) . 0 = 0 by A3;

hence lim ((h ") (#) (cf /* h)) = 0 by A7, SEQ_4:25; :: thesis: verum

set L = cf;

for p being Real holds cf . p = 0 * p ;

then reconsider L = cf as LinearFunc by Def3;

f | Z is V8() ;

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;

A9: now :: thesis: for x0 being Real st x0 in Z holds

f is_differentiable_in x0

set x0 = the Element of REAL ;f is_differentiable_in x0

let x0 be Real; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )

reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;

assume x0 in Z ; :: thesis: f is_differentiable_in x0

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

end;reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;

assume x0 in Z ; :: thesis: f is_differentiable_in x0

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

proof

hence
f is_differentiable_in x0
; :: thesis: verum
let x be Real; :: thesis: ( x in the Neighbourhood of x0 implies (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )

reconsider xx = x as Element of REAL by XREAL_0:def 1;

assume x in the Neighbourhood of x0 ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

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: verum

end;reconsider xx = x as Element of REAL by XREAL_0:def 1;

assume x in the Neighbourhood of x0 ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

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: verum

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: ( R . 0 = 0 & R is_continuous_in 0 )

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: R is_continuous_in 0

A16: now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds

( R /* h is convergent & lim (R /* h) = R . 0 )

( R /* h is convergent & lim (R /* h) = R . 0 )

set s3 = seq_const 0;

let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( R /* h is convergent & lim (R /* h) = R . 0 )

A17: (seq_const 0) . 1 = 0 ;

(h ") (#) (R /* h) is convergent by Def2;

then (h ") (#) (R /* h) is bounded ;

then consider M being Real such that

M > 0 and

A18: for n being Nat holds |.(((h ") (#) (R /* h)) . n).| < M by SEQ_2:3;

then lim (abs h) = |.0.| by SEQ_4:14

.= 0 by ABSVALUE:2 ;

then A22: lim (M (#) (abs h)) = M * 0 by SEQ_2:8

.= lim (seq_const 0) by A17, SEQ_4:25 ;

A23: abs (R /* h) is convergent by A22, A19, SEQ_2:19;

lim (seq_const 0) = 0 by A17, SEQ_4:25;

then lim (abs (R /* h)) = 0 by A22, A19, SEQ_2:20;

hence ( R /* h is convergent & lim (R /* h) = R . 0 ) by A15, A23, SEQ_4:15; :: thesis: verum

end;let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( R /* h is convergent & lim (R /* h) = R . 0 )

A17: (seq_const 0) . 1 = 0 ;

(h ") (#) (R /* h) is convergent by Def2;

then (h ") (#) (R /* h) is bounded ;

then consider M being Real such that

M > 0 and

A18: for n being Nat holds |.(((h ") (#) (R /* h)) . n).| < M by SEQ_2:3;

A19: now :: thesis: for n being Nat holds

( (seq_const 0) . n <= (abs (R /* h)) . n & (abs (R /* h)) . n <= (M (#) (abs h)) . n )

lim h = 0
;( (seq_const 0) . n <= (abs (R /* h)) . n & (abs (R /* h)) . n <= (M (#) (abs h)) . n )

let n be Nat; :: thesis: ( (seq_const 0) . n <= (abs (R /* h)) . n & (abs (R /* h)) . n <= (M (#) (abs h)) . n )

|.(((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: (abs (R /* h)) . n <= (M (#) (abs h)) . n

|.(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: verum

end;|.(((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: (abs (R /* h)) . n <= (M (#) (abs h)) . n

|.(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: verum

then lim (abs h) = |.0.| by SEQ_4:14

.= 0 by ABSVALUE:2 ;

then A22: lim (M (#) (abs h)) = M * 0 by SEQ_2:8

.= lim (seq_const 0) by A17, SEQ_4:25 ;

A23: abs (R /* h) is convergent by A22, A19, SEQ_2:19;

lim (seq_const 0) = 0 by A17, SEQ_4:25;

then lim (abs (R /* h)) = 0 by A22, A19, SEQ_2:20;

hence ( R /* h is convergent & lim (R /* h) = R . 0 ) by A15, A23, SEQ_4:15; :: thesis: verum

now :: thesis: for s1 being Real_Sequence st rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being Nat holds s1 . n <> 0 ) holds

( R /* s1 is convergent & lim (R /* s1) = R . 0 )

hence
R is_continuous_in 0
by FCONT_1:2; :: thesis: verum( R /* s1 is convergent & lim (R /* s1) = R . 0 )

let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being Nat holds s1 . n <> 0 ) implies ( R /* s1 is convergent & lim (R /* s1) = R . 0 ) )

assume that

rng s1 c= dom R and

A24: ( s1 is convergent & lim s1 = 0 ) and

A25: for n being Nat holds s1 . n <> 0 ; :: thesis: ( R /* s1 is convergent & lim (R /* s1) = R . 0 )

s1 is 0 -convergent by A24;

then s1 is non-zero 0 -convergent Real_Sequence by A25, SEQ_1:5;

hence ( R /* s1 is convergent & lim (R /* s1) = R . 0 ) by A16; :: thesis: verum

end;assume that

rng s1 c= dom R and

A24: ( s1 is convergent & lim s1 = 0 ) and

A25: for n being Nat holds s1 . n <> 0 ; :: thesis: ( R /* s1 is convergent & lim (R /* s1) = R . 0 )

s1 is 0 -convergent by A24;

then s1 is non-zero 0 -convergent Real_Sequence by A25, SEQ_1:5;

hence ( R /* s1 is convergent & lim (R /* s1) = R . 0 ) by A16; :: thesis: verum