let S, T be RealNormSpace; 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; 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; 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; ( 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 )
; for i being Nat st i <= n holds
diff ((- f),i,Z) = - (diff (f,i,Z))
let i be Nat; ( i <= n implies diff ((- f),i,Z) = - (diff (f,i,Z)) )
assume
i <= n
; 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; verum