let S be RealNormSpace-Sequence; :: thesis: for T being RealNormSpace
for Z being Subset of (product S)
for f being PartFunc of (product S),T
for a being Real
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( - f is_partial_differentiable_on Z,i & (- f) `partial| (Z,i) = - (f `partial| (Z,i)) )
let T be RealNormSpace; :: thesis: for Z being Subset of (product S)
for f being PartFunc of (product S),T
for a being Real
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( - f is_partial_differentiable_on Z,i & (- f) `partial| (Z,i) = - (f `partial| (Z,i)) )
let Z be Subset of (product S); :: thesis: for f being PartFunc of (product S),T
for a being Real
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( - f is_partial_differentiable_on Z,i & (- f) `partial| (Z,i) = - (f `partial| (Z,i)) )
let f be PartFunc of (product S),T; :: thesis: for a being Real
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( - f is_partial_differentiable_on Z,i & (- f) `partial| (Z,i) = - (f `partial| (Z,i)) )
let a be Real; :: thesis: for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i holds
( - f is_partial_differentiable_on Z,i & (- f) `partial| (Z,i) = - (f `partial| (Z,i)) )
let i be set ; :: thesis: ( Z is open & i in dom S & f is_partial_differentiable_on Z,i implies ( - f is_partial_differentiable_on Z,i & (- f) `partial| (Z,i) = - (f `partial| (Z,i)) ) )
assume that
A1: ( Z is open & i in dom S ) and
A2: f is_partial_differentiable_on Z,i ; :: thesis: ( - f is_partial_differentiable_on Z,i & (- f) `partial| (Z,i) = - (f `partial| (Z,i)) )
A3: - f = (- 1) (#) f by VFUNCT_1:23;
hence - f is_partial_differentiable_on Z,i by A1, A2, Th27; :: thesis: (- f) `partial| (Z,i) = - (f `partial| (Z,i))
( (- 1) (#) f is_partial_differentiable_on Z,i & ((- 1) (#) f) `partial| (Z,i) = (- 1) (#) (f `partial| (Z,i)) ) by A1, A2, Th27;
hence (- f) `partial| (Z,i) = - (f `partial| (Z,i)) by A3, VFUNCT_1:23; :: thesis: verum