let F be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of F
for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
let f be PartFunc of REAL, the carrier of F; :: thesis: for x0 being Real st f is_differentiable_in x0 holds
f is_continuous_in x0
let x0 be Real; :: thesis: ( f is_differentiable_in x0 implies f is_continuous_in x0 )
assume A1: f is_differentiable_in x0 ; :: thesis: f is_continuous_in x0
then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ;
A3: x0 in N by RCOMP_1:16;

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

consider g being Real such that
A4: 0 < g and
A5: N = ].(x0 - g),(x0 + g).[ by RCOMP_1:def 6;
reconsider xx = x0 as Element of REAL by XREAL_0:def 1;
set s2 = seq_const x0;
let s1 be Real_Sequence; :: thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) )
assume that
A6: rng s1 c= dom f and
A7: s1 is convergent and
A8: lim s1 = x0 and
A9: for n being Nat holds s1 . n <> x0 ; :: thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) )
consider l being Nat such that
A10: for m being Nat st l <= m holds
|.((s1 . m) - x0).| < g by A7, A8, A4, SEQ_2:def 7;
reconsider c = (seq_const x0) ^\ l as constant Real_Sequence ;
deffunc H₁( Real) -> set = (s1 . $1) - ((seq_const x0) . $1);
consider s3 being Real_Sequence such that
A11: for n being Nat holds s3 . n = H₁(n) from SEQ_1:sch 1();
A12: s3 = s1 - (seq_const x0) by A11, RFUNCT_2:1;
then A13: s3 is convergent by A7;
A14: rng c = {x0}

proof

thus rng c c= {x0} :: according to XBOOLE_0:def 10 :: thesis: {x0} c= rng c

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in {x0} )
assume y in rng c ; :: thesis: y in {x0}
then consider n being Element of NAT such that
A15: y = ((seq_const x0) ^\ l) . n by FUNCT_2:113;
y = (seq_const x0) . (n + l) by A15, NAT_1:def 3;
then y = x0 by SEQ_1:57;
hence y in {x0} by TARSKI:def 1; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {x0} or y in rng c )
assume y in {x0} ; :: thesis: y in rng c
then A16: y = x0 by TARSKI:def 1;
reconsider z0 = 0 as Element of NAT ;
c . z0 = (seq_const x0) . (z0 + l) by NAT_1:def 3
.= y by A16, SEQ_1:57 ;
hence y in rng c by VALUED_0:28; :: thesis: verum

end;

A17: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p )
assume A18: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p
reconsider n = 0 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p
let m be Nat; :: thesis: ( n <= m implies ||.(((f /* c) . m) - (f /. x0)).|| < p )
assume n <= m ; :: thesis: ||.(((f /* c) . m) - (f /. x0)).|| < p
A19: m in NAT by ORDINAL1:def 12;
x0 in N by RCOMP_1:16;
then rng c c= dom f by A2, A14, ZFMISC_1:31;
then ||.(((f /* c) . m) - (f /. x0)).|| = ||.((f /. (c . m)) - (f /. x0)).|| by FUNCT_2:109, A19
.= ||.((f /. ((seq_const x0) . (m + l))) - (f /. x0)).|| by NAT_1:def 3
.= ||.((f /. x0) - (f /. x0)).|| by SEQ_1:57
.= ||.(0. F).|| by RLVECT_1:15
.= 0 ;
hence ||.(((f /* c) . m) - (f /. x0)).|| < p by A18; :: thesis: verum

end;

then A20: f /* c is convergent by NORMSP_1:def 6;
lim (seq_const x0) = (seq_const x0) . 0 by SEQ_4:26
.= x0 by SEQ_1:57 ;
then lim s3 = x0 - x0 by A7, A8, A12, SEQ_2:12
.= 0 ;
then A21: lim (s3 ^\ l) = 0 by A13, SEQ_4:20;

A22: now :: thesis: for n being Element of NAT holds not s3 . n = 0

given n being Element of NAT such that A23: s3 . n = 0 ; :: thesis: contradiction
(s1 . n) - ((seq_const x0) . n) = 0 by A11, A23;
hence contradiction by A9, SEQ_1:57; :: thesis: verum

end;

A24: now :: thesis: for n being Nat holds not (s3 ^\ l) . n = 0

given n being Nat such that A25: (s3 ^\ l) . n = 0 ; :: thesis: contradiction
A26: n + l in NAT by ORDINAL1:def 12;
s3 . (n + l) = 0 by A25, NAT_1:def 3;
hence contradiction by A22, A26; :: thesis: verum

end;

then s3 ^\ l is non-zero by SEQ_1:5;
then reconsider h = s3 ^\ l as non-zero 0 -convergent Real_Sequence by A13, A21, FDIFF_1:def 1;

now :: thesis: for n being Element of NAT holds (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (f /* (h + c)) . n

let n be Element of NAT ; :: thesis: (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (f /* (h + c)) . n
thus (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n) by NORMSP_1:def 2
.= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by NORMSP_1:def 3
.= ((f /* (h + c)) . n) - (((f /* c) . n) - ((f /* c) . n)) by RLVECT_1:29
.= ((f /* (h + c)) . n) - (0. F) by RLVECT_1:15
.= (f /* (h + c)) . n by RLVECT_1:13 ; :: thesis: verum

end;

then A27: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c) by FUNCT_2:63;

now :: thesis: for n being Element of NAT holds (h + c) . n = (s1 ^\ l) . n

let n be Element of NAT ; :: thesis: (h + c) . n = (s1 ^\ l) . n
thus (h + c) . n = (((s1 - (seq_const x0)) + (seq_const x0)) ^\ l) . n by A12, SEQM_3:15
.= ((s1 - (seq_const x0)) + (seq_const x0)) . (n + l) by NAT_1:def 3
.= ((s1 - (seq_const x0)) . (n + l)) + ((seq_const x0) . (n + l)) by SEQ_1:7
.= ((s1 . (n + l)) - ((seq_const x0) . (n + l))) + ((seq_const x0) . (n + l)) by RFUNCT_2:1
.= (s1 ^\ l) . n by NAT_1:def 3 ; :: thesis: verum

end;

then A28: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (s1 ^\ l) by A27, FUNCT_2:63
.= (f /* s1) ^\ l by A6, VALUED_0:27 ;

now :: thesis: for y being object st y in rng (h + c) holds
y in N

let y be object ; :: thesis: ( y in rng (h + c) implies y in N )
assume y in rng (h + c) ; :: thesis: y in N
then consider n being Element of NAT such that
A29: y = (h + c) . n by FUNCT_2:113;
(h + c) . n = (((s1 - (seq_const x0)) + (seq_const x0)) ^\ l) . n by A12, SEQM_3:15
.= ((s1 - (seq_const x0)) + (seq_const x0)) . (n + l) by NAT_1:def 3
.= ((s1 - (seq_const x0)) . (n + l)) + ((seq_const x0) . (n + l)) by SEQ_1:7
.= ((s1 . (n + l)) - ((seq_const x0) . (n + l))) + ((seq_const x0) . (n + l)) by RFUNCT_2:1
.= s1 . (l + n) ;
then |.(((h + c) . n) - x0).| < g by A10, NAT_1:12;
hence y in N by A5, A29, RCOMP_1:1; :: thesis: verum

end;

then A30: rng (h + c) c= N ;
A31: lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = 0 * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A21, A1, A2, A14, Th13, A30, NDIFF_1:14
.= 0. F by RLVECT_1:10 ;

now :: thesis: for n being Element of NAT holds (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n

let n be Element of NAT ; :: thesis: (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n
A32: h . n <> 0 by A24;
thus (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = (h . n) * (((h ") (#) ((f /* (h + c)) - (f /* c))) . n) by NDIFF_1:def 2
.= (h . n) * (((h ") . n) * (((f /* (h + c)) - (f /* c)) . n)) by NDIFF_1:def 2
.= (h . n) * (((h . n) ") * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:10
.= ((h . n) * ((h . n) ")) * (((f /* (h + c)) - (f /* c)) . n) by RLVECT_1:def 7
.= 1 * (((f /* (h + c)) - (f /* c)) . n) by A32, XCMPLX_0:def 7
.= ((f /* (h + c)) - (f /* c)) . n by RLVECT_1:def 8 ; :: thesis: verum

end;

then A33: h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c) by FUNCT_2:63;
then A34: (f /* (h + c)) - (f /* c) is convergent by A30, A1, A2, A14, Th13, NDIFF_1:13;
then ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A20, NORMSP_1:19;
hence f /* s1 is convergent by A28, LOPBAN_3:10; :: thesis: f /. x0 = lim (f /* s1)
lim (f /* c) = f /. x0 by A17, A20, NORMSP_1:def 7;
then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = (0. F) + (f /. x0) by A31, A33, A34, A20, NORMSP_1:25
.= f /. x0 by RLVECT_1:4 ;
hence f /. x0 = lim (f /* s1) by A34, A28, A20, LOPBAN_3:11, NORMSP_1:19; :: thesis: verum

end;

hence f is_continuous_in x0 by A3, A2, NFCONT_3:7; :: thesis: verum