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 ) )
A1: - f = (- 1) (#) f ;
assume A2: f is_differentiable_on n,Z ; :: thesis: ( (diff (- f),Z) . n = - ((diff f,Z) . n) & - f is_differentiable_on n,Z )
then (diff (- f),Z) . n = (- 1) (#) ((diff f,Z) . n) by Th21
.= - ((diff f,Z) . n) ;
hence ( (diff (- f),Z) . n = - ((diff f,Z) . n) & - f is_differentiable_on n,Z ) by A2, A1, Th22; :: thesis: verum