theorem Th14: :: INTEGR26:14

for f being PartFunc of REAL,REAL
for I being open Subset of REAL
for X being Subset of REAL st I c= X holds
( f is_differentiable_on I iff f | X is_differentiable_on I )