theorem :: FDIFF_12:32

for f being PartFunc of REAL,REAL
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