theorem :: HFDIFF_1:23

for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on Z holds
(diff (f,Z)) . 1 = f `| Z