let n be non zero Element of NAT ; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds
( - f is_differentiable_on Z & ( for x being Real st x in Z holds
((- f) `| Z) . x = - (diff (f,x)) ) )
let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,(REAL n) st Z c= dom f & f is_differentiable_on Z holds
( - f is_differentiable_on Z & ( for x being Real st x in Z holds
((- f) `| Z) . x = - (diff (f,x)) ) )
let f be PartFunc of REAL,(REAL n); :: thesis: ( Z c= dom f & f is_differentiable_on Z implies ( - f is_differentiable_on Z & ( for x being Real st x in Z holds
((- f) `| Z) . x = - (diff (f,x)) ) ) )
(- 1) (#) f = - f by NFCONT_4:7;
hence ( Z c= dom f & f is_differentiable_on Z implies ( - f is_differentiable_on Z & ( for x being Real st x in Z holds
((- f) `| Z) . x = - (diff (f,x)) ) ) ) by Th13; :: thesis: verum