let f be PartFunc of REAL ,REAL ; :: thesis: for x0 being Real st f is_left_differentiable_in x0 holds
f is_Lcontinuous_in x0
let x0 be Real; :: thesis: ( f is_left_differentiable_in x0 implies f is_Lcontinuous_in x0 )
assume A1: f is_left_differentiable_in x0 ; :: thesis: f is_Lcontinuous_in x0
A2: x0 in dom f

proof

consider r being Real such that
A3: ( 0 < r & [.(x0 - r),x0.] c= dom f ) by A1, Def4;
x0 - r <= x0 by A3, XREAL_1:46;
then x0 in [.(x0 - r),x0.] by XXREAL_1:1;
hence x0 in dom f by A3; :: thesis: verum

end;

for a being Real_Sequence st rng a c= (left_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds
( f /* a is convergent & f . x0 = lim (f /* a) )

proof

let a be Real_Sequence; :: thesis: ( rng a c= (left_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 implies ( f /* a is convergent & f . x0 = lim (f /* a) ) )
assume A4: ( rng a c= (left_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 ) ; :: thesis: ( f /* a is convergent & f . x0 = lim (f /* a) )
consider r being Real such that
A5: ( 0 < r & [.(x0 - r),x0.] c= dom f ) by A1, Def4;
x0 - r < x0 by A5, XREAL_1:46;
then consider n0 being Element of NAT such that
A6: for k being Element of NAT st k >= n0 holds
x0 - r < a . k by A4, LIMFUNC2:1;
A7: for n being Element of NAT holds (a ^\ n0) . n in [.(x0 - r),x0.]

proof

let n be Element of NAT ; :: thesis: (a ^\ n0) . n in [.(x0 - r),x0.]
( 0 <= n & 0 + n0 = n0 ) by NAT_1:2;
then n0 <= n0 + n by XREAL_1:8;
then x0 - r <= a . (n + n0) by A6;
then A8: x0 - r <= (a ^\ n0) . n by NAT_1:def 3;
a . (n + n0) in rng a by VALUED_0:28;
then (a ^\ n0) . n in rng a by NAT_1:def 3;
then (a ^\ n0) . n in left_open_halfline x0 by A4, XBOOLE_0:def 4;
then (a ^\ n0) . n in { g where g is Real : g < x0 } by XXREAL_1:229;
then ex g being Real st
( g = (a ^\ n0) . n & g < x0 ) ;
then (a ^\ n0) . n in { g where g is Real : ( x0 - r <= g & g <= x0 ) } by A8;
hence (a ^\ n0) . n in [.(x0 - r),x0.] by RCOMP_1:def 1; :: thesis: verum

end;

reconsider b = NAT --> x0 as Real_Sequence ;
deffunc H₁( Element of NAT ) -> Element of REAL = (a . $1) - (b . $1);
consider d being Real_Sequence such that
A9: for n being Element of NAT holds d . n = H₁(n) from SEQ_1:sch 1();
A11: lim b = b . 0 by SEQ_4:41
.= x0 by FUNCOP_1:13 ;
A12: d = a - b by A9, RFUNCT_2:6;
then A13: d is convergent by A4, SEQ_2:25;
lim d = x0 - x0 by A4, A11, A12, SEQ_2:26
.= 0 ;
then A14: ( d ^\ n0 is convergent & lim (d ^\ n0) = 0 ) by A13, SEQ_4:33;
A15: for n being Element of NAT holds
( d . n < 0 & d . n <> 0 )

proof

let n be Element of NAT ; :: thesis: ( d . n < 0 & d . n <> 0 )
A16: d . n = (a . n) - (b . n) by A9;
a . n in rng a by VALUED_0:28;
then a . n in left_open_halfline x0 by A4, XBOOLE_0:def 4;
then a . n in { r1 where r1 is Real : r1 < x0 } by XXREAL_1:229;
then A17: ex r1 being Real st
( r1 = a . n & r1 < x0 ) ;
then (a . n) - x0 < x0 - x0 by XREAL_1:11;
hence d . n < 0 by A16, FUNCOP_1:13; :: thesis: d . n <> 0
thus d . n <> 0 by A16, A17, FUNCOP_1:13; :: thesis: verum

end;

A18: for n being Element of NAT holds (d ^\ n0) . n < 0

proof

let n be Element of NAT ; :: thesis: (d ^\ n0) . n < 0
(d ^\ n0) . n = d . (n + n0) by NAT_1:def 3;
hence (d ^\ n0) . n < 0 by A15; :: thesis: verum

end;

then for n being Element of NAT holds (d ^\ n0) . n <> 0 ;
then d ^\ n0 is non-zero by SEQ_1:7;
then reconsider h = d ^\ n0 as convergent_to_0 Real_Sequence by A14, FDIFF_1:def 1;
reconsider c = b ^\ n0 as V8() Real_Sequence ;
A19: rng c = {x0}

proof

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in {x0} )
assume x in rng c ; :: thesis: x in {x0}
then consider n being Element of NAT such that
A20: x = (b ^\ n0) . n by FUNCT_2:190;
x = b . (n + n0) by A20, NAT_1:def 3;
then x = x0 by FUNCOP_1:13;
hence x in {x0} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {x0} or x in rng c )
assume x in {x0} ; :: thesis: x in rng c
then A21: x = x0 by TARSKI:def 1;
c . 0 = b . (0 + n0) by NAT_1:def 3
.= x by A21, FUNCOP_1:13 ;
hence x in rng c by VALUED_0:28; :: thesis: verum

end;

rng (h + c) c= [.(x0 - r),x0.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (h + c) or x in [.(x0 - r),x0.] )
assume x in rng (h + c) ; :: thesis: x in [.(x0 - r),x0.]
then consider n being Element of NAT such that
A22: x = (h + c) . n by FUNCT_2:190;
(h + c) . n = (((a - b) + b) ^\ n0) . n by A12, SEQM_3:37
.= ((a - b) + b) . (n + n0) by NAT_1:def 3
.= ((a - b) . (n + n0)) + (b . (n + n0)) by SEQ_1:11
.= ((a . (n + n0)) - (b . (n + n0))) + (b . (n + n0)) by RFUNCT_2:6
.= (a ^\ n0) . n by NAT_1:def 3 ;
hence x in [.(x0 - r),x0.] by A7, A22; :: thesis: verum

end;

then rng (h + c) c= dom f by A5, XBOOLE_1:1;
then A23: (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A18, A19, Def4;
then A24: lim (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = 0 * (lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) by A14, SEQ_2:29
.= 0 ;

now

let n be Element of NAT ; :: thesis: (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n
A25: h . n <> 0 by A18;
thus (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c)))) . n = (h . n) * (((h " ) (#) ((f /* (h + c)) - (f /* c))) . n) by SEQ_1:12
.= (h . n) * (((h " ) . n) * (((f /* (h + c)) - (f /* c)) . n)) by SEQ_1:12
.= (h . n) * (((h . n) " ) * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:10
.= ((h . n) * ((h . n) " )) * (((f /* (h + c)) - (f /* c)) . n)
.= 1 * (((f /* (h + c)) - (f /* c)) . n) by A25, XCMPLX_0:def 7
.= ((f /* (h + c)) - (f /* c)) . n ; :: thesis: verum

end;

then A26: h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c) by FUNCT_2:113;
then A27: (f /* (h + c)) - (f /* c) is convergent by A14, A23, SEQ_2:28;

A28: now

let g be real number ; :: thesis: ( 0 < g implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* c) . m) - (f . x0)) < g )
assume A29: 0 < g ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* c) . m) - (f . x0)) < g
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
abs (((f /* c) . m) - (f . x0)) < g
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((f /* c) . m) - (f . x0)) < g )
assume n <= m ; :: thesis: abs (((f /* c) . m) - (f . x0)) < g
x0 - r <= x0 by A5, XREAL_1:46;
then x0 in [.(x0 - r),x0.] by XXREAL_1:1;
then rng c c= dom f by A5, A19, ZFMISC_1:37;
then abs (((f /* c) . m) - (f . x0)) = abs ((f . (c . m)) - (f . x0)) by FUNCT_2:185
.= abs ((f . (b . (m + n0))) - (f . x0)) by NAT_1:def 3
.= abs ((f . x0) - (f . x0)) by FUNCOP_1:13
.= 0 by ABSVALUE:7 ;
hence abs (((f /* c) . m) - (f . x0)) < g by A29; :: thesis: verum

end;

then A30: f /* c is convergent by SEQ_2:def 6;
then A31: lim (f /* c) = f . x0 by A28, SEQ_2:def 7;
A32: ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A27, A30, SEQ_2:19;
A33: lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = 0 + (f . x0) by A24, A26, A27, A30, A31, SEQ_2:20
.= f . x0 ;

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 SEQ_1:11
.= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by RFUNCT_2:6
.= (f /* (h + c)) . n ; :: thesis: verum

end;

then A34: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c) by FUNCT_2:113;
A35: rng a c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng a or x in dom f )
assume x in rng a ; :: thesis: x in dom f
hence x in dom f by A4, XBOOLE_0:def 4; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: (h + c) . n = (a ^\ n0) . n
thus (h + c) . n = (((a - b) + b) ^\ n0) . n by A12, SEQM_3:37
.= ((a - b) + b) . (n + n0) by NAT_1:def 3
.= ((a - b) . (n + n0)) + (b . (n + n0)) by SEQ_1:11
.= ((a . (n + n0)) - (b . (n + n0))) + (b . (n + n0)) by RFUNCT_2:6
.= (a ^\ n0) . n by NAT_1:def 3 ; :: thesis: verum

end;

then A36: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (a ^\ n0) by A34, FUNCT_2:113
.= (f /* a) ^\ n0 by A35, VALUED_0:27 ;
hence f /* a is convergent by A32, SEQ_4:35; :: thesis: f . x0 = lim (f /* a)
thus f . x0 = lim (f /* a) by A32, A33, A36, SEQ_4:36; :: thesis: verum

end;

hence f is_Lcontinuous_in x0 by A2, Def1; :: thesis: verum