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

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