let f be PartFunc of REAL,REAL; :: thesis: for Z being Subset of REAL st f is_differentiable_on Z holds
(- f) `| Z = - (f `| Z)
let Z be Subset of REAL; :: thesis: ( f is_differentiable_on Z implies (- f) `| Z = - (f `| Z) )
assume A1: f is_differentiable_on Z ; :: thesis: (- f) `| Z = - (f `| Z)
Z is open Subset of REAL by A1, FDIFF_1:10;
then (- f) `| Z = (- 1) (#) (f `| Z) by A1, FDIFF_2:19
.= - (f `| Z) ;
hence (- f) `| Z = - (f `| Z) ; :: thesis: verum