theorem Th35: :: FDIFF_12:35

for f being PartFunc of REAL,REAL
for x0 being Real st f is_Rcontinuous_in x0 holds
f | (right_closed_halfline x0) is_continuous_in x0