theorem :: HFDIFF_1:33

for n being Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds
( (diff ((- f),Z)) . n = - ((diff (f,Z)) . n) & - f is_differentiable_on n,Z ) by Th21, Th22;