let F be non trivial RealNormSpace; :: thesis: ex R being REST of F st
( R /. 0 = 0. F & 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 Lm1, RCOMP_1:def 5;
set R = REAL --> (0. F);
reconsider f = REAL --> (0. F) as PartFunc of REAL, the carrier of F ;
A1: dom (REAL --> (0. F)) = REAL by FUNCOP_1:13;

now

let h be convergent_to_0 Real_Sequence; :: thesis: ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F )

now

let n be Nat; :: thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F
A2: rng h c= dom (REAL --> (0. F)) by A1;
A3: n in NAT by ORDINAL1:def 12;
hence ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def 2
.= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108
.= 0. F by FUNCOP_1:7, RLVECT_1:10 ;
:: thesis: verum

end;

then ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def 18;
hence ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; :: thesis: verum

end;

then reconsider R = REAL --> (0. F) as REST of F by Def1;
set L = REAL --> (0. F);

now

let p be Real; :: thesis: (REAL --> (0. F)) . p = p * (0. F)
thus (REAL --> (0. F)) . p = 0. F by FUNCOP_1:7
.= p * (0. F) by RLVECT_1:10 ; :: thesis: verum

end;

then reconsider L = REAL --> (0. F) as LINEAR of F by Def2;
A4: Z c= dom f by FUNCOP_1:13;
A5: f | Z is constant ;
consider r being Point of F such that
A6: for x being Real st x in Z /\ (dom f) holds
f . x = r by A5, PARTFUN2:57;

A7: now

let x be Real; :: thesis: ( x in Z /\ (dom f) implies f /. x = r )
assume A8: x in Z /\ (dom f) ; :: thesis: f /. x = r
then x in dom f by XBOOLE_0:def 4;
hence f /. x = f . x by PARTFUN1:def 6
.= r by A8, A6 ;
:: thesis: verum

end;

A9: now

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;
A10: the Neighbourhood of x0 c= dom f by A4, XBOOLE_1:1;
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)) )
A11: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def 6
.= 0. F by FUNCOP_1:7 ;
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 A10, XBOOLE_0:def 4;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A7
.= r - r by A7, A1
.= 0. F by RLVECT_1:15
.= L . (x - x0) by FUNCOP_1:7
.= (L . (x - x0)) + (R /. (x - x0)) by A11, RLVECT_1:4 ;
:: thesis: verum

end;

hence f is_differentiable_in x0 by A10, Def3; :: thesis: verum

end;

set x0 = the Real;
f is_differentiable_in the Real by A9;
then consider N being Neighbourhood of the Real such that
N c= dom f and
A12: ex L being LINEAR of F ex R being REST of F st
for x being Real st x in N holds
(f /. x) - (f /. the Real) = (L . (x - the Real)) + (R /. (x - the Real)) by Def3;
consider L being LINEAR of F, R being REST of F such that
A13: for x being Real st x in N holds
(f /. x) - (f /. the Real) = (L . (x - the Real)) + (R /. (x - the Real)) by A12;
take R ; :: thesis: ( R /. 0 = 0. F & R is_continuous_in 0 )
consider p being Point of F such that
A14: for r being Real holds L . r = r * p by Def2;
(f /. the Real) - (f /. the Real) = (L . ( the Real - the Real)) + (R /. ( the Real - the Real)) by A13, RCOMP_1:16;
then 0. F = (L . ( the Real - the Real)) + (R /. ( the Real - the Real)) by RLVECT_1:15;
then 0. F = (0 * p) + (R /. 0) by A14;
then 0. F = (0. F) + (R /. 0) by RLVECT_1:10;
hence A15: R /. 0 = 0. F by RLVECT_1:4; :: thesis: R is_continuous_in 0

A16: now

set s3 = cs;
let h be convergent_to_0 Real_Sequence; :: thesis: ( R /* h is convergent & lim (R /* h) = R /. 0 )
A17: cs . 1 = 0 by FUNCOP_1:7;
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0. F ) by Def1;
then ||.((h ") (#) (R /* h)).|| is bounded by LOPBAN_1:20, SEQ_2:13;
then consider M being real number such that
M > 0 and
A18: for n being Element of NAT holds abs (||.((h ") (#) (R /* h)).|| . n) < M by SEQ_2:3;

A19: now

let n be Element of NAT ; :: thesis: ||.(((h ") (#) (R /* h)) . n).|| < M
abs (||.((h ") (#) (R /* h)).|| . n) < M by A18;
then abs ||.(((h ") (#) (R /* h)) . n).|| < M by NORMSP_0:def 4;
hence ||.(((h ") (#) (R /* h)) . n).|| < M by ABSVALUE:def 1; :: thesis: verum

end;

A20: h is convergent by FDIFF_1:def 1;
then A21: abs h is convergent by SEQ_4:13;
A22: h is non-empty by FDIFF_1:def 1;
reconsider z0 = 0 as Real ;

A23: now

let n be Element of NAT ; :: thesis: ||.((R /* h) . n).|| <= (M (#) (abs h)) . n
||.(((h ") (#) (R /* h)) . n).|| = ||.(((h ") . n) * ((R /* h) . n)).|| by NDIFF_1:def 2
.= ||.(((h . n) ") * ((R /* h) . n)).|| by VALUED_1:10 ;
then A24: ||.(((h . n) ") * ((R /* h) . n)).|| <= M by A19;
abs (h . n) >= 0 by COMPLEX1:46;
then (abs (h . n)) * ||.(((h . n) ") * ((R /* h) . n)).|| <= M * (abs (h . n)) by A24, XREAL_1:64;
then ||.((h . n) * (((h . n) ") * ((R /* h) . n))).|| <= M * (abs (h . n)) by NORMSP_1:def 1;
then A25: ||.(((h . n) * ((h . n) ")) * ((R /* h) . n)).|| <= M * (abs (h . n)) by RLVECT_1:def 7;
h . n <> 0 by A22, SEQ_1:5;
then ||.(1 * ((R /* h) . n)).|| <= M * (abs (h . n)) by A25, XCMPLX_0:def 7;
then ||.((R /* h) . n).|| <= M * (abs (h . n)) by RLVECT_1:def 8;
then ||.((R /* h) . n).|| <= M * ((abs h) . n) by SEQ_1:12;
hence ||.((R /* h) . n).|| <= (M (#) (abs h)) . n by SEQ_1:9; :: thesis: verum

end;

lim h = z0 by FDIFF_1:def 1;
then lim (abs h) = abs z0 by A20, SEQ_4:14
.= z0 by ABSVALUE:2 ;
then A26: lim (M (#) (abs h)) = M * z0 by A21, SEQ_2:8
.= lim cs by A17, SEQ_4:25 ;
A27: M (#) (abs h) is convergent by A21, SEQ_2:7;
reconsider z0 = 0 as Real ;
lim (M (#) (abs h)) = 0 by A26, A17, SEQ_4:25;
hence ( R /* h is convergent & lim (R /* h) = R /. 0 ) by A15, A27, A23, Th1; :: thesis: verum

end;

R is total by Def1;
then A28: dom R = REAL by FUNCT_2:def 1;

now

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 & R /. 0 = lim (R /* s1) ) )
assume that
rng s1 c= dom R and
A29: ( s1 is convergent & lim s1 = 0 ) and
A30: for n being Element of NAT holds s1 . n <> 0 ; :: thesis: ( R /* s1 is convergent & R /. 0 = lim (R /* s1) )
s1 is non-empty by A30, SEQ_1:5;
then s1 is convergent_to_0 Real_Sequence by A29, FDIFF_1:def 1;
hence ( R /* s1 is convergent & R /. 0 = lim (R /* s1) ) by A16; :: thesis: verum

end;

hence R is_continuous_in 0 by A28, NFCONT_3:7; :: thesis: verum