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 that
A1: f is_continuous_in x0 and
A2: 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 :: thesis: for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} holds
( f /* s is convergent & lim (f /* s) = f . x0 )

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 that
A3: ( s is convergent & lim s = x0 ) and
A4: 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 A4;
hence ( f /* s is convergent & lim (f /* s) = f . x0 ) by A1, A3, FCONT_1:def 1; :: thesis: verum

end;

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