let f be PartFunc of REAL , REAL ; :: thesis: for x0 being Real st f is_continuous_in x0 & ( 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 ) ) holds
f is_convergent_in x0
let x0 be Real; :: thesis: ( f is_continuous_in x0 & ( 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 ) ) implies f is_convergent_in x0 )
assume A1: ( f is_continuous_in x0 & ( 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 ) ) ) ; :: thesis: f is_convergent_in x0

now

let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} implies ( f /* s is convergent & lim (f /* s) = f . x0 ) )
assume A2: ( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} ) ; :: thesis: ( f /* s is convergent & lim (f /* s) = f . x0 )
(dom f) \ {x0} c= dom f by XBOOLE_1:36;
then rng s c= dom f by A2, XBOOLE_1:1;
hence ( f /* s is convergent & lim (f /* s) = f . x0 ) by A1, A2, FCONT_1:def 1; :: thesis: verum

end;

hence f is_convergent_in x0 by A1, LIMFUNC3:def 1; :: thesis: verum