theorem :: HFDIFF_1:24

for n being Element of NAT
for Z being open Subset of REAL
for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds
(diff (f1,Z)) . 1 = f1 `| Z