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
- f is_differentiable_on n,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
- f is_differentiable_on n,Z
let n be Nat; :: thesis: for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
- f is_differentiable_on n,Z
let f be PartFunc of S,T; :: thesis: ( 1 <= n & f is_differentiable_on n,Z implies - f is_differentiable_on n,Z )
assume ( 1 <= n & f is_differentiable_on n,Z ) ; :: thesis: - f is_differentiable_on n,Z
then (- 1) (#) f is_differentiable_on n,Z by Th25;
hence - f is_differentiable_on n,Z by VFUNCT_1:23; :: thesis: verum