theorem Th10: :: NDIFF_4:10

for x0 being Real
for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n) st f is_differentiable_in x0 holds
( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) )