theorem Th12: :: INTEGR26:12

for x being Real
for f being PartFunc of REAL,REAL
for I being non empty Interval
for X being Subset of REAL st I c= X & x in I & x <> sup I holds
( f is_right_differentiable_in x iff f | X is_right_differentiable_in x )