let S, T be RealNormSpace; :: thesis: for Z being Subset of S
for n being Nat
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((- f),i,Z) = - (diff (f,i,Z))
let Z be Subset of S; :: thesis: for n being Nat
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((- f),i,Z) = - (diff (f,i,Z))
let n be Nat; :: thesis: for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((- f),i,Z) = - (diff (f,i,Z))
let f be PartFunc of S,T; :: thesis: ( 1 <= n & f is_differentiable_on n,Z implies for i being Nat st i <= n holds
diff ((- f),i,Z) = - (diff (f,i,Z)) )
assume A1: ( 1 <= n & f is_differentiable_on n,Z ) ; :: thesis: for i being Nat st i <= n holds
diff ((- f),i,Z) = - (diff (f,i,Z))
let i be Nat; :: thesis: ( i <= n implies diff ((- f),i,Z) = - (diff (f,i,Z)) )
assume i <= n ; :: thesis: diff ((- f),i,Z) = - (diff (f,i,Z))
then diff (((- 1) (#) f),i,Z) = (- 1) (#) (diff (f,i,Z)) by Th24, A1;
then (diff (((- 1) (#) f),Z)) . i = - (diff (f,i,Z)) by VFUNCT_1:23;
hence diff ((- f),i,Z) = - (diff (f,i,Z)) by VFUNCT_1:23; :: thesis: verum