let S be RealNormSpace-Sequence; :: thesis: for T being RealNormSpace
for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I holds
( - f is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((- f),Z,I,i) = - (PartDiffSeq (f,Z,I,i)) ) )
let T be RealNormSpace; :: thesis: for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I holds
( - f is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((- f),Z,I,i) = - (PartDiffSeq (f,Z,I,i)) ) )
let Z be Subset of (product S); :: thesis: for I being non empty FinSequence of dom S
for f being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I holds
( - f is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((- f),Z,I,i) = - (PartDiffSeq (f,Z,I,i)) ) )
let I be non empty FinSequence of dom S; :: thesis: for f being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I holds
( - f is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((- f),Z,I,i) = - (PartDiffSeq (f,Z,I,i)) ) )
let f be PartFunc of (product S),T; :: thesis: ( Z is open & f is_partial_differentiable_on Z,I implies ( - f is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((- f),Z,I,i) = - (PartDiffSeq (f,Z,I,i)) ) ) )
assume that
A1: Z is open and
A2: f is_partial_differentiable_on Z,I ; :: thesis: ( - f is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((- f),Z,I,i) = - (PartDiffSeq (f,Z,I,i)) ) )
A3: (- 1) (#) f = - f by VFUNCT_1:23;
hence - f is_partial_differentiable_on Z,I by A1, A2, Th31; :: thesis: for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((- f),Z,I,i) = - (PartDiffSeq (f,Z,I,i))
let i be Nat; :: thesis: ( 1 <= i & i <= len I implies PartDiffSeq ((- f),Z,I,i) = - (PartDiffSeq (f,Z,I,i)) )
assume ( 1 <= i & i <= len I ) ; :: thesis: PartDiffSeq ((- f),Z,I,i) = - (PartDiffSeq (f,Z,I,i))
hence PartDiffSeq ((- f),Z,I,i) = (- 1) (#) (PartDiffSeq (f,Z,I,i)) by A1, A2, A3, Th31
.= - (PartDiffSeq (f,Z,I,i)) by VFUNCT_1:23 ;
:: thesis: verum