theorem Th18: :: PDLAX:12

for f being PartFunc of REAL,REAL
for X, Z being Subset of REAL st Z is open & Z c= X & f is_differentiable_on X holds
f `| Z = (f `| X) | Z