let x0 be Real; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
assume A1: f is_convergent_in x0 ; :: thesis:

A2: now :: thesis:

let s be Real_Sequence; :: thesis:
assume that
A3: s is convergent and
A4: lim s = x0 and
A5: rng s c= (dom f) /\ (right_open_halfline x0) ; :: thesis:
rng s c= (dom f) \ {x0} by A5, Th1;
hence ( f /* s is convergent & lim (f /* s) = lim (f,x0) ) by A1, A3, A4, Def4; :: thesis:

end;

A6: now :: thesis:

let s be Real_Sequence; :: thesis:
assume that
A7: s is convergent and
A8: lim s = x0 and
A9: rng s c= (dom f) /\ (left_open_halfline x0) ; :: thesis:
rng s c= (dom f) \ {x0} by A9, Th1;
hence ( f /* s is convergent & lim (f /* s) = lim (f,x0) ) by A1, A7, A8, Def4; :: thesis:

end;

A10: 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;
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 A6, LIMFUNC2:def 1; :: thesis:
then A11: lim_left (f,x0) = lim (f,x0) by A6, 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 A10, Th8;
hence f is_right_convergent_in x0 by A2, LIMFUNC2:def 4; :: thesis:
hence ( lim_left (f,x0) = lim_right (f,x0) & lim (f,x0) = lim_left (f,x0) & lim (f,x0) = lim_right (f,x0) ) by A11, A2, LIMFUNC2:def 8; :: thesis: