theorem Th22: :: INTEGRA8:22

for f1 being PartFunc of REAL,REAL
for x0 being Real st f1 is_differentiable_in x0 holds
( - f1 is_differentiable_in x0 & diff ((- f1),x0) = - (diff (f1,x0)) )