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