let a, b, x be Real; :: thesis: for f being PartFunc of REAL,REAL st [.a,b.] c= dom f & f | [.a,b.] is continuous & x in ].a,b.] holds
( f is_left_convergent_in x & lim_left ((f | ].a,b.[),x) = f . x )
let f be PartFunc of REAL,REAL; :: thesis: ( [.a,b.] c= dom f & f | [.a,b.] is continuous & x in ].a,b.] implies ( f is_left_convergent_in x & lim_left ((f | ].a,b.[),x) = f . x ) )
assume that
A1: [.a,b.] c= dom f and
A2: f | [.a,b.] is continuous and
A3: x in ].a,b.] ; :: thesis: ( f is_left_convergent_in x & lim_left ((f | ].a,b.[),x) = f . x )
A4: ( a < x & x <= b ) by A3, XXREAL_1:2;
A5: for r being Real st r < x holds
ex g being Real st
( r < g & g < x & g in dom f )

proof

let r be Real; :: thesis: ( r < x implies ex g being Real st
( r < g & g < x & g in dom f ) )
set r1 = max (r,a);
assume r < x ; :: thesis: ex g being Real st
( r < g & g < x & g in dom f )
then consider g being Real such that
A6: ( max (r,a) < g & g < x ) by A4, XXREAL_0:29, XREAL_1:5;
r <= max (r,a) by XXREAL_0:25;
then A7: r < g by A6, XXREAL_0:2;
a <= max (r,a) by XXREAL_0:25;
then ( a <= g & g < b ) by A4, A6, XXREAL_0:2;
then g in [.a,b.] by XXREAL_1:1;
hence ex g being Real st
( r < g & g < x & g in dom f ) by A1, A6, A7; :: thesis: verum

end;

A8: dom (f | [.a,b.]) = [.a,b.] by A1, RELAT_1:62;
A9: ].a,b.] c= [.a,b.] by XXREAL_1:23;
].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A10: ].a,b.[ c= dom f by A1;
A11: for r being Real st 0 < r holds
ex s being Real st
( s < x & ( for x1 being Real st s < x1 & x1 < x & x1 in dom f holds
|.((f . x1) - (f . x)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( s < x & ( for x1 being Real st s < x1 & x1 < x & x1 in dom f holds
|.((f . x1) - (f . x)).| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( s < x & ( for x1 being Real st s < x1 & x1 < x & x1 in dom f holds
|.((f . x1) - (f . x)).| < r ) )
then consider e being Real such that
A12: ( 0 < e & ( for x1 being Real st x1 in dom (f | [.a,b.]) & |.(x1 - x).| < e holds
|.(((f | [.a,b.]) . x1) - ((f | [.a,b.]) . x)).| < r ) ) by A9, A2, A3, A8, FCONT_1:def 2, FCONT_1:3;
set s1 = x - e;
set s = max ((x - e),a);
A13: ( x - e <= max ((x - e),a) & a <= max ((x - e),a) ) by XXREAL_0:25;
A14: x - e < x by A12, XREAL_1:44;
take max ((x - e),a) ; :: thesis: ( max ((x - e),a) < x & ( for x1 being Real st max ((x - e),a) < x1 & x1 < x & x1 in dom f holds
|.((f . x1) - (f . x)).| < r ) )
thus max ((x - e),a) < x by A4, A14, XXREAL_0:29; :: thesis: for x1 being Real st max ((x - e),a) < x1 & x1 < x & x1 in dom f holds
|.((f . x1) - (f . x)).| < r

hereby :: thesis: verum

let x1 be Real; :: thesis: ( max ((x - e),a) < x1 & x1 < x & x1 in dom f implies |.((f . x1) - (f . x)).| < r )
assume that
A15: max ((x - e),a) < x1 and
A16: x1 < x and
x1 in dom f ; :: thesis: |.((f . x1) - (f . x)).| < r
A17: (max ((x - e),a)) - x < x1 - x by A15, XREAL_1:9;
(x - e) - x <= (max ((x - e),a)) - x by XXREAL_0:25, XREAL_1:9;
then (x - e) - x < x1 - x by A17, XXREAL_0:2;
then A18: - (x1 - x) < - ((x - e) - x) by XREAL_1:24;
x1 - x < 0 by A16, XREAL_1:49;
then A19: |.(x1 - x).| < e by A18, ABSVALUE:30;
x <= b by A9, A3, XXREAL_1:1;
then A20: ( a < x1 & x1 < b ) by A15, A13, A16, XXREAL_0:2;
then A21: x1 in dom (f | [.a,b.]) by A8, XXREAL_1:1;
( (f | [.a,b.]) . x1 = f . x1 & (f | [.a,b.]) . x = f . x ) by A9, A20, A8, A3, XXREAL_1:1, FUNCT_1:47;
hence |.((f . x1) - (f . x)).| < r by A12, A19, A21; :: thesis: verum

end;

end;

hence A22: f is_left_convergent_in x by A5, LIMFUNC2:7; :: thesis: lim_left ((f | ].a,b.[),x) = f . x
A23: for r being Real st 0 < r holds
ex s being Real st
( s < x & ( for x1 being Real st s < x1 & x1 < x & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (f . x)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( s < x & ( for x1 being Real st s < x1 & x1 < x & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (f . x)).| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( s < x & ( for x1 being Real st s < x1 & x1 < x & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (f . x)).| < r ) )
then consider s0 being Real such that
A24: ( s0 < x & ( for x1 being Real st s0 < x1 & x1 < x & x1 in dom f holds
|.((f . x1) - (f . x)).| < r ) ) by A11;
set s = max (s0,a);
for x1 being Real st max (s0,a) < x1 & x1 < x & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (f . x)).| < r

proof

let x1 be Real; :: thesis: ( max (s0,a) < x1 & x1 < x & x1 in dom (f | ].a,b.[) implies |.(((f | ].a,b.[) . x1) - (f . x)).| < r )
assume that
A25: max (s0,a) < x1 and
A26: x1 < x and
A27: x1 in dom (f | ].a,b.[) ; :: thesis: |.(((f | ].a,b.[) . x1) - (f . x)).| < r
s0 <= max (s0,a) by XXREAL_0:25;
then A28: s0 < x1 by A25, XXREAL_0:2;
x1 in dom f by A27, RELAT_1:57;
then |.((f . x1) - (f . x)).| < r by A24, A28, A26;
hence |.(((f | ].a,b.[) . x1) - (f . x)).| < r by A27, FUNCT_1:47; :: thesis: verum

end;

hence ex s being Real st
( s < x & ( for x1 being Real st s < x1 & x1 < x & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (f . x)).| < r ) ) by A24, A4, XXREAL_0:29; :: thesis: verum

end;

A29: ( f | ].a,b.[ is_left_convergent_in x & lim_left ((f | ].a,b.[),x) = lim_left (f,x) ) by A4, A22, A10, Th9;
thus lim_left ((f | ].a,b.[),x) = f . x by A23, A29, LIMFUNC2:41; :: thesis: verum