let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_left_convergent_in x0 holds
( ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_below ) & ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_above ) )
let x0 be Real; :: thesis: ( f is_left_convergent_in x0 implies ( ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_below ) & ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_above ) ) )
assume A1: f is_left_convergent_in x0 ; :: thesis: ( ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_below ) & ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_above ) )
consider g being Real such that
A2: for g1 being Real st 0 < g1 holds
ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) by A1, LIMFUNC2:7;
consider r being Real such that
A3: r < x0 and
A4: for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
|.((f . r1) - g).| < 1 by A2;
set R = x0 - r;
for r1 being object st r1 in dom (f | ].(x0 - (x0 - r)),x0.[) holds
(- 1) + g < (f | ].(x0 - (x0 - r)),x0.[) . r1

proof

let r1 be object ; :: thesis: ( r1 in dom (f | ].(x0 - (x0 - r)),x0.[) implies (- 1) + g < (f | ].(x0 - (x0 - r)),x0.[) . r1 )
assume A5: r1 in dom (f | ].(x0 - (x0 - r)),x0.[) ; :: thesis: (- 1) + g < (f | ].(x0 - (x0 - r)),x0.[) . r1
then reconsider r1 = r1 as Real ;
r1 in (dom f) /\ ].(x0 - (x0 - r)),x0.[ by A5, RELAT_1:61;
then A6: ( r1 in dom f & r1 in ].(x0 - (x0 - r)),x0.[ ) by XBOOLE_0:def 4;
then A7: ( x0 - (x0 - r) < r1 & r1 < x0 ) by XXREAL_1:4;
then |.((f . r1) - g).| < 1 by A4, A6;
then A8: - 1 <= (f . r1) - g by ABSVALUE:5;

now :: thesis: not - 1 = (f . r1) - g

assume - 1 = (f . r1) - g ; :: thesis: contradiction
then |.((f . r1) - g).| = - (- 1) by ABSVALUE:def 1;
hence contradiction by A7, A4, A6; :: thesis: verum

end;

then - 1 < (f . r1) - g by A8, XXREAL_0:1;
then (- 1) + g < f . r1 by XREAL_1:20;
hence (- 1) + g < (f | ].(x0 - (x0 - r)),x0.[) . r1 by A6, FUNCT_1:49; :: thesis: verum

end;

then f | ].(x0 - (x0 - r)),x0.[ is bounded_below by SEQ_2:def 2;
hence ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_below ) by A3, XREAL_1:50; :: thesis: ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_above )
consider r being Real such that
A9: r < x0 and
A10: for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
|.((f . r1) - g).| < 1 by A2;
set R = x0 - r;
for r1 being object st r1 in dom (f | ].(x0 - (x0 - r)),x0.[) holds
(f | ].(x0 - (x0 - r)),x0.[) . r1 < g + 1

proof

let r1 be object ; :: thesis: ( r1 in dom (f | ].(x0 - (x0 - r)),x0.[) implies (f | ].(x0 - (x0 - r)),x0.[) . r1 < g + 1 )
assume A11: r1 in dom (f | ].(x0 - (x0 - r)),x0.[) ; :: thesis: (f | ].(x0 - (x0 - r)),x0.[) . r1 < g + 1
then reconsider r1 = r1 as Real ;
r1 in (dom f) /\ ].(x0 - (x0 - r)),x0.[ by A11, RELAT_1:61;
then A12: ( r1 in dom f & r1 in ].(x0 - (x0 - r)),x0.[ ) by XBOOLE_0:def 4;
then ( r1 < x0 & x0 - (x0 - r) < r1 ) by XXREAL_1:4;
then |.((f . r1) - g).| < 1 by A10, A12;
then (f . r1) - g < 1 by ABSVALUE:def 1;
then f . r1 < g + 1 by XREAL_1:19;
hence (f | ].(x0 - (x0 - r)),x0.[) . r1 < g + 1 by A12, FUNCT_1:49; :: thesis: verum

end;

then f | ].(x0 - (x0 - r)),x0.[ is bounded_above by SEQ_2:def 1;
hence ex r being Real st
( 0 < r & f | ].(x0 - r),x0.[ is bounded_above ) by A9, XREAL_1:50; :: thesis: verum