let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st x0 in dom f & f is_right_convergent_in x0 & lim_right (f,x0) = f . x0 holds
f is_Rcontinuous_in x0
let x0 be Real; :: thesis: ( x0 in dom f & f is_right_convergent_in x0 & lim_right (f,x0) = f . x0 implies f is_Rcontinuous_in x0 )
assume that
A1: x0 in dom f and
A2: f is_right_convergent_in x0 and
A3: lim_right (f,x0) = f . x0 ; :: thesis: f is_Rcontinuous_in x0
for a being Real_Sequence st rng a c= (right_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds
( f /* a is convergent & f . x0 = lim (f /* a) ) by A2, A3, LIMFUNC2:def 8;
hence f is_Rcontinuous_in x0 by A1, FDIFF_3:def 2; :: thesis: verum