let T, S be non trivial RealNormSpace; :: thesis: for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
f is_continuous_in x0
let f be PartFunc of S,T; :: thesis: for x0 being Point of S st f is_differentiable_in x0 holds
f is_continuous_in x0
let x0 be Point of S; :: 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 Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by Def6;

A3: now

consider g being Real such that
A4: 0 < g and
A5: { y where y is Point of S : ||.(y - x0).|| < g } c= N by NFCONT_1:def 1;
reconsider s2 = NAT --> x0 as sequence of S ;
let s1 be sequence of S; :: thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of 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 Element of NAT holds s1 . n <> x0 ; :: thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) )
consider l being Element of NAT such that
A10: for m being Element of NAT st l <= m holds
||.((s1 . m) - x0).|| < g by A7, A8, A4, NORMSP_1:def 7;
deffunc H₁( Element of NAT ) -> Element of the carrier of S = (s1 . $1) - (s2 . $1);
consider s3 being sequence of S such that
A11: for n being Element of NAT holds s3 . n = H₁(n) from FUNCT_2:sch 4();

A12: now

given n being Element of NAT such that A13: s3 . n = 0. S ; :: thesis: contradiction
(s1 . n) - (s2 . n) = 0. S by A11, A13;
then (s1 . n) - x0 = 0. S by FUNCOP_1:7;
hence contradiction by A9, RLVECT_1:21; :: thesis: verum

end;

now

given n being Element of NAT such that A14: (s3 ^\ l) . n = 0. S ; :: thesis: contradiction
s3 . (n + l) = 0. S by A14, NAT_1:def 3;
hence contradiction by A12; :: thesis: verum

end;

then A15: s3 ^\ l is non-zero by Th7;
reconsider c = s2 ^\ l as constant sequence of S ;
A16: s3 = s1 - s2 by A11, NORMSP_1:def 3;
A17: s2 is convergent by Th21;
then A18: s3 is convergent by A7, A16, NORMSP_1:20;
then A19: s3 ^\ l is convergent by LOPBAN_3:9;
lim s2 = s2 . 0 by Th21
.= x0 by FUNCOP_1:7 ;
then lim s3 = x0 - x0 by A7, A8, A17, A16, NORMSP_1:26
.= 0. S by RLVECT_1:15 ;
then lim (s3 ^\ l) = 0. S by A18, LOPBAN_3:9;
then reconsider h = s3 ^\ l as convergent_to_0 sequence of S by A19, A15, Def4;

now

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. T) by RLVECT_1:15
.= (f /* (h + c)) . n by RLVECT_1:13 ; :: thesis: verum

end;

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

now

let n be Element of NAT ; :: thesis: (h + c) . n = (s1 ^\ l) . n
thus (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A16, Th15
.= ((s1 - s2) + s2) . (n + l) by NAT_1:def 3
.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by NORMSP_1:def 2
.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by NORMSP_1:def 3
.= (s1 . (n + l)) - ((s2 . (n + l)) - (s2 . (n + l))) by RLVECT_1:29
.= (s1 . (n + l)) - (0. S) by RLVECT_1:15
.= s1 . (l + n) by RLVECT_1:13
.= (s1 ^\ l) . n by NAT_1:def 3 ; :: thesis: verum

end;

then A21: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (s1 ^\ l) by A20, FUNCT_2:63
.= (f /* s1) ^\ l by A6, VALUED_0:27 ;
A22: rng c = {x0}

proof

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

proof

let y be set ; :: 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
A23: y = (s2 ^\ l) . n by NFCONT_1:6;
y = s2 . (n + l) by A23, NAT_1:def 3;
then y = x0 by FUNCOP_1:7;
hence y in {x0} by TARSKI:def 1; :: thesis: verum

end;

let y be set ; :: 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 A24: y = x0 by TARSKI:def 1;
c . 0 = s2 . (0 + l) by NAT_1:def 3
.= y by A24, FUNCOP_1:7 ;
hence y in rng c by NFCONT_1:6; :: thesis: verum

end;

A25: now

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p )
assume A26: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
||.(((f /* c) . m) - (f /. x0)).|| < p
let m be Element of NAT ; :: thesis: ( n <= m implies ||.(((f /* c) . m) - (f /. x0)).|| < p )
assume n <= m ; :: thesis: ||.(((f /* c) . m) - (f /. x0)).|| < p
x0 in N by NFCONT_1:4;
then rng c c= dom f by A2, A22, ZFMISC_1:31;
then ||.(((f /* c) . m) - (f /. x0)).|| = ||.((f /. (c . m)) - (f /. x0)).|| by FUNCT_2:109
.= ||.((f /. (s2 . (m + l))) - (f /. x0)).|| by NAT_1:def 3
.= ||.((f /. x0) - (f /. x0)).|| by FUNCOP_1:7
.= ||.(0. T).|| by RLVECT_1:15
.= 0 by NORMSP_1:1 ;
hence ||.(((f /* c) . m) - (f /. x0)).|| < p by A26; :: thesis: verum

end;

then A27: f /* c is convergent by NORMSP_1:def 6;
A28: rng (h + c) c= N

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (h + c) or y in N )
assume A29: y in rng (h + c) ; :: thesis: y in N
then consider n being Element of NAT such that
A30: y = (h + c) . n by NFCONT_1:6;
reconsider y1 = y as Point of S by A29;
(h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A16, Th15
.= ((s1 - s2) + s2) . (n + l) by NAT_1:def 3
.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by NORMSP_1:def 2
.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by NORMSP_1:def 3
.= (s1 . (n + l)) - ((s2 . (n + l)) - (s2 . (n + l))) by RLVECT_1:29
.= (s1 . (n + l)) - (0. S) by RLVECT_1:15
.= s1 . (l + n) by RLVECT_1:13 ;
then ||.(((h + c) . n) - x0).|| < g by A10, NAT_1:12;
then y1 in { z where z is Point of S : ||.(z - x0).|| < g } by A30;
hence y in N by A5; :: thesis: verum

end;

then A31: (f /* (h + c)) - (f /* c) is convergent by A1, A2, A22, Th39;
then ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A27, NORMSP_1:19;
hence f /* s1 is convergent by A21, LOPBAN_3:10; :: thesis: f /. x0 = lim (f /* s1)
A32: lim ((f /* (h + c)) - (f /* c)) = 0. T by A1, A2, A22, A28, Th39;
lim (f /* c) = f /. x0 by A25, A27, NORMSP_1:def 7;
then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = (0. T) + (f /. x0) by A31, A32, A27, NORMSP_1:25
.= f /. x0 by RLVECT_1:4 ;
hence f /. x0 = lim (f /* s1) by A31, A27, A21, LOPBAN_3:11, NORMSP_1:19; :: thesis: verum

end;

x0 in N by NFCONT_1:4;
hence f is_continuous_in x0 by A2, A3, Th32; :: thesis: verum