theorem :: FDIFF_12:17

for f being PartFunc of REAL,REAL
for x0 being Real st dom f c= right_open_halfline x0 & f is_Rcontinuous_in x0 holds
f is_continuous_in x0