let x0 be Real; :: thesis: 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)) )
let n be non zero Element of NAT ; :: thesis: 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)) )
let f be PartFunc of REAL,(REAL n); :: thesis: ( f is_differentiable_in x0 implies ( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) ) )
(- 1) (#) f = - f by NFCONT_4:7;
hence ( f is_differentiable_in x0 implies ( - f is_differentiable_in x0 & diff ((- f),x0) = - (diff (f,x0)) ) ) by Th9; :: thesis: verum