:: deftheorem defines is_Rcontinuous_in FDIFF_3:def 2 :
for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_Rcontinuous_in x0 iff ( x0 in dom f & ( 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) ) ) ) );