A1: {} REAL is closed

proof

let a be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not K87(a) c= {} REAL or not a is convergent or lim a in {} REAL )
assume ( rng a c= {} REAL & a is convergent ) ; :: thesis: lim a in {} REAL
hence lim a in {} REAL by XBOOLE_1:3; :: thesis: verum

end;

( ([#] 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;
set R = cf;
reconsider f = cf as PartFunc of REAL,REAL ;
A2: dom cf = REAL by FUNCOP_1:13;

now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (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 )

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

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

end;

then A6: (h ") (#) (cf /* h) is V8() by VALUED_0:def 18;
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 A6, SEQ_4:25; :: thesis: verum

end;

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

A8: now :: thesis: for x0 being Real st x0 in Z holds
f is_differentiable_in x0

let x0 be Real; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume x0 in Z ; :: thesis: f is_differentiable_in x0
set N = the Neighbourhood of x0;
A9: the Neighbourhood of x0 c= dom f by A2;
A10: x0 in Z /\ (dom f) by A2;
for x being Real st x in the Neighbourhood of x0 holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))

proof

let x be Real; :: thesis: ( x in the Neighbourhood of x0 implies (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) )
assume x in the Neighbourhood of x0 ; :: thesis: (f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0))
then x in Z /\ (dom f) by A9, XBOOLE_0:def 4;
hence (f . x) - (f . x0) = r - (f . x0) by A7
.= r - r by A7, A10
.= (L . (x - x0)) + 0 by FUNCOP_1:7
.= (L . (x - x0)) + (R . (x - x0)) by FUNCOP_1:7 ;
:: thesis: verum

end;

hence f is_differentiable_in x0 by A9, Def4; :: thesis: verum

end;

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

A15: now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( R /* h is convergent & lim (R /* h) = R . 0 )

set s3 = cs;
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( R /* h is convergent & lim (R /* h) = R . 0 )
A16: cs . 1 = 0 by FUNCOP_1:7;
(h ") (#) (R /* h) is convergent by Def2;
then (h ") (#) (R /* h) is bounded by SEQ_2:13;
then consider M being real number such that
M > 0 and
A17: for n being Element of NAT holds abs (((h ") (#) (R /* h)) . n) < M by SEQ_2:3;

A18: now :: thesis: for n being Element of NAT holds
( cs . n <= (abs (R /* h)) . n & (abs (R /* h)) . n <= (M (#) (abs h)) . n )

let n be Element of NAT ; :: thesis: ( cs . n <= (abs (R /* h)) . n & (abs (R /* h)) . n <= (M (#) (abs h)) . n )
abs (((h ") (#) (R /* h)) . n) = abs (((h ") . n) * ((R /* h) . n)) by SEQ_1:8
.= abs (((h . n) ") * ((R /* h) . n)) by VALUED_1:10 ;
then A19: abs (((h . n) ") * ((R /* h) . n)) <= M by A17;
0 <= abs ((R /* h) . n) by COMPLEX1:46;
then 0 <= (abs (R /* h)) . n by SEQ_1:12;
hence cs . n <= (abs (R /* h)) . n by FUNCOP_1:7; :: thesis: (abs (R /* h)) . n <= (M (#) (abs h)) . n
abs (h . n) >= 0 by COMPLEX1:46;
then (abs (h . n)) * (abs (((h . n) ") * ((R /* h) . n))) <= M * (abs (h . n)) by A19, XREAL_1:64;
then abs ((h . n) * (((h . n) ") * ((R /* h) . n))) <= M * (abs (h . n)) by COMPLEX1:65;
then A20: abs (((h . n) * ((h . n) ")) * ((R /* h) . n)) <= M * (abs (h . n)) ;
h . n <> 0 by SEQ_1:5;
then abs (1 * ((R /* h) . n)) <= M * (abs (h . n)) by A20, XCMPLX_0:def 7;
then abs ((R /* h) . n) <= M * ((abs h) . n) by SEQ_1:12;
then abs ((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;

lim h = 0 ;
then lim (abs h) = abs 0 by SEQ_4:14
.= 0 by ABSVALUE:2 ;
then A21: lim (M (#) (abs h)) = M * 0 by SEQ_2:8
.= lim cs by A16, SEQ_4:25 ;
A22: M (#) (abs h) is convergent by SEQ_2:7;
then A23: abs (R /* h) is convergent by A21, A18, SEQ_2:19;
lim cs = 0 by A16, SEQ_4:25;
then lim (abs (R /* h)) = 0 by A22, A21, A18, SEQ_2:20;
hence ( R /* h is convergent & lim (R /* h) = R . 0 ) by A14, A23, SEQ_4:15; :: thesis: verum

end;

now :: thesis: for s1 being Real_Sequence st rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being Element of NAT holds s1 . n <> 0 ) holds
( 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 Element of 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 Element of NAT holds s1 . n <> 0 ; :: thesis: ( R /* s1 is convergent & lim (R /* s1) = R . 0 )
s1 is 0 -convergent by A24, Def1;
then s1 is non-zero 0 -convergent Real_Sequence by SEQ_1:5, A25;
hence ( R /* s1 is convergent & lim (R /* s1) = R . 0 ) by A15; :: thesis: verum

end;

hence R is_continuous_in 0 by FCONT_1:2; :: thesis: verum