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

proof

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

end;

A8: for r being Real st 0 < r holds
ex d being Real st
( d < x & ( for x1 being Real st d < x1 & x1 < x & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (lim_left (f,x))).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex d being Real st
( d < x & ( for x1 being Real st d < x1 & x1 < x & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (lim_left (f,x))).| < r ) ) )
assume 0 < r ; :: thesis: ex d being Real st
( d < x & ( for x1 being Real st d < x1 & x1 < x & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (lim_left (f,x))).| < r ) )
then consider d0 being Real such that
A9: ( d0 < x & ( for x1 being Real st d0 < x1 & x1 < x & x1 in dom f holds
|.((f . x1) - (lim_left (f,x))).| < r ) ) by A3, LIMFUNC2:41;
set d = max (d0,a);
for x1 being Real st max (d0,a) < x1 & x1 < x & x1 in dom (f | ].a,b.[) holds
|.(((f | ].a,b.[) . x1) - (lim_left (f,x))).| < r

proof

let x1 be Real; :: thesis: ( max (d0,a) < x1 & x1 < x & x1 in dom (f | ].a,b.[) implies |.(((f | ].a,b.[) . x1) - (lim_left (f,x))).| < r )
assume that
A10: max (d0,a) < x1 and
A11: x1 < x and
A12: x1 in dom (f | ].a,b.[) ; :: thesis: |.(((f | ].a,b.[) . x1) - (lim_left (f,x))).| < r
d0 <= max (d0,a) by XXREAL_0:25;
then A13: d0 < x1 by A10, XXREAL_0:2;
x1 in dom f by A12, RELAT_1:57;
then |.((f . x1) - (lim_left (f,x))).| < r by A13, A11, A9;
hence |.(((f | ].a,b.[) . x1) - (lim_left (f,x))).| < r by A12, FUNCT_1:47; :: thesis: verum

end;

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

end;

hence f | ].a,b.[ is_left_convergent_in x by A5, LIMFUNC2:7; :: thesis: lim_left ((f | ].a,b.[),x) = lim_left (f,x)
hence lim_left ((f | ].a,b.[),x) = lim_left (f,x) by A8, LIMFUNC2:41; :: thesis: verum