let x0 be Real; :: thesis: for f being PartFunc of REAL ,REAL st f is_convergent_in x0 holds
( f is_left_convergent_in x0 & f is_right_convergent_in x0 & lim_left f,x0 = lim_right f,x0 & lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_convergent_in x0 implies ( f is_left_convergent_in x0 & f is_right_convergent_in x0 & lim_left f,x0 = lim_right f,x0 & lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 ) )
assume A1: f is_convergent_in x0 ; :: thesis: ( f is_left_convergent_in x0 & f is_right_convergent_in x0 & lim_left f,x0 = lim_right f,x0 & lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 )
A2: lim f,x0 = lim f,x0 ;
A3: for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) by A1, Def1;
then A4: for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) by Th8;

A5: now

let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) /\ (left_open_halfline x0) implies ( f /* s is convergent & lim (f /* s) = lim f,x0 ) )
assume A6: ( s is convergent & lim s = x0 & rng s c= (dom f) /\ (left_open_halfline x0) ) ; :: thesis: ( f /* s is convergent & lim (f /* s) = lim f,x0 )
then rng s c= (dom f) \ {x0} by Th1;
hence ( f /* s is convergent & lim (f /* s) = lim f,x0 ) by A1, A2, A6, Def4; :: thesis: verum

end;

hence f is_left_convergent_in x0 by A4, LIMFUNC2:def 1; :: thesis: ( f is_right_convergent_in x0 & lim_left f,x0 = lim_right f,x0 & lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 )
then A7: lim_left f,x0 = lim f,x0 by A5, LIMFUNC2:def 7;
A8: for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) by A3, Th8;

A9: now

let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) /\ (right_open_halfline x0) implies ( f /* s is convergent & lim (f /* s) = lim f,x0 ) )
assume A10: ( s is convergent & lim s = x0 & rng s c= (dom f) /\ (right_open_halfline x0) ) ; :: thesis: ( f /* s is convergent & lim (f /* s) = lim f,x0 )
then rng s c= (dom f) \ {x0} by Th1;
hence ( f /* s is convergent & lim (f /* s) = lim f,x0 ) by A1, A2, A10, Def4; :: thesis: verum

end;

hence f is_right_convergent_in x0 by A8, LIMFUNC2:def 4; :: thesis: ( lim_left f,x0 = lim_right f,x0 & lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 )
hence ( lim_left f,x0 = lim_right f,x0 & lim f,x0 = lim_left f,x0 & lim f,x0 = lim_right f,x0 ) by A7, A9, LIMFUNC2:def 8; :: thesis: verum