let n be Element of NAT ; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st f is_differentiable_on n,Z holds
( (diff (- f),Z) . n = - ((diff f,Z) . n) & - f is_differentiable_on n,Z )
let Z be open Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st f is_differentiable_on n,Z holds
( (diff (- f),Z) . n = - ((diff f,Z) . n) & - f is_differentiable_on n,Z )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_differentiable_on n,Z implies ( (diff (- f),Z) . n = - ((diff f,Z) . n) & - f is_differentiable_on n,Z ) )
assume A1: f is_differentiable_on n,Z ; :: thesis: ( (diff (- f),Z) . n = - ((diff f,Z) . n) & - f is_differentiable_on n,Z )
A2: (diff (- f),Z) . n = (- 1) (#) ((diff f,Z) . n) by A1, Th13
.= - ((diff f,Z) . n) ;
- f = (- 1) (#) f ;
hence ( (diff (- f),Z) . n = - ((diff f,Z) . n) & - f is_differentiable_on n,Z ) by A2, Th14, A1; :: thesis: verum