theorem Th9: :: FDIFF_12:9

for f being PartFunc of REAL,REAL
for I being Interval
for x being Real st f | I is_right_differentiable_in x holds
( f is_right_differentiable_in x & Rdiff ((f | I),x) = Rdiff (f,x) )