let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st dom f c= right_open_halfline x0 & f is_Rcontinuous_in x0 holds
f is_continuous_in x0
let x0 be Real; :: thesis: ( dom f c= right_open_halfline x0 & f is_Rcontinuous_in x0 implies f is_continuous_in x0 )
assume that
A1: dom f c= right_open_halfline x0 and
A2: f is_Rcontinuous_in x0 ; :: thesis: f is_continuous_in x0
for s being Real_Sequence st rng s c= dom f & s is convergent & lim s = x0 holds
( f /* s is convergent & f . x0 = lim (f /* s) )

proof

let s be Real_Sequence; :: thesis: ( rng s c= dom f & s is convergent & lim s = x0 implies ( f /* s is convergent & f . x0 = lim (f /* s) ) )
assume that
A3: rng s c= dom f and
A4: s is convergent and
A5: lim s = x0 ; :: thesis: ( f /* s is convergent & f . x0 = lim (f /* s) )
rng s c= right_open_halfline x0 by A1, A3;
then rng s c= (right_open_halfline x0) /\ (dom f) by A3, XBOOLE_1:19;
hence ( f /* s is convergent & f . x0 = lim (f /* s) ) by A4, A5, A2, FDIFF_3:def 2; :: thesis: verum

end;

hence f is_continuous_in x0 by FCONT_1:def 1; :: thesis: verum