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: 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 that
A4: s is convergent and
A5: lim s = x0 and
A6: rng s c= (dom f) /\ (right_open_halfline x0) ; :: thesis: ( f /* s is convergent & lim (f /* s) = lim (f,x0) )
rng s c= (dom f) \ {x0} by A6, Th1;
hence ( f /* s is convergent & lim (f /* s) = lim (f,x0) ) by A1, A2, A4, A5, Def4; :: thesis: verum

end;

A7: 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 that
A8: s is convergent and
A9: lim s = x0 and
A10: rng s c= (dom f) /\ (left_open_halfline x0) ; :: thesis: ( f /* s is convergent & lim (f /* s) = lim (f,x0) )
rng s c= (dom f) \ {x0} by A10, Th1;
hence ( f /* s is convergent & lim (f /* s) = lim (f,x0) ) by A1, A2, A8, A9, Def4; :: thesis: verum

end;

A11: 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 for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) by Th8;
hence f is_left_convergent_in x0 by A7, 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 A12: lim_left (f,x0) = lim (f,x0) by A7, LIMFUNC2:def 7;
for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) by A11, Th8;
hence f is_right_convergent_in x0 by A3, 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 A12, A3, LIMFUNC2:def 8; :: thesis: verum