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, g being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f - g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f - g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) - (PartDiffSeq (g,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, g being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f - g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f - g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) - (PartDiffSeq (g,Z,I,i)) ) )
let Z be Subset of (product S); :: thesis: for I being non empty FinSequence of dom S
for f, g being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f - g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f - g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) - (PartDiffSeq (g,Z,I,i)) ) )
let I be non empty FinSequence of dom S; :: thesis: for f, g being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f - g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f - g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) - (PartDiffSeq (g,Z,I,i)) ) )
let f, g be PartFunc of (product S),T; :: thesis: ( Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I implies ( f - g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f - g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) - (PartDiffSeq (g,Z,I,i)) ) ) )
assume that
A1: Z is open and
A2: f is_partial_differentiable_on Z,I and
A3: g is_partial_differentiable_on Z,I ; :: thesis: ( f - g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f - g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) - (PartDiffSeq (g,Z,I,i)) ) )
A4: f - g = f + (- g) by VFUNCT_1:25;
A5: ( - g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((- g),Z,I,i) = - (PartDiffSeq (g,Z,I,i)) ) ) by A1, A3, Th32;
hence f - g is_partial_differentiable_on Z,I by A1, A2, A4, Th30; :: thesis: for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f - g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) - (PartDiffSeq (g,Z,I,i))
let i be Nat; :: thesis: ( 1 <= i & i <= len I implies PartDiffSeq ((f - g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) - (PartDiffSeq (g,Z,I,i)) )
assume A6: ( 1 <= i & i <= len I ) ; :: thesis: PartDiffSeq ((f - g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) - (PartDiffSeq (g,Z,I,i))
hence PartDiffSeq ((f - g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq ((- g),Z,I,i)) by A1, A2, A4, A5, Th30
.= (PartDiffSeq (f,Z,I,i)) + (- (PartDiffSeq (g,Z,I,i))) by A1, A3, A6, Th32
.= (PartDiffSeq (f,Z,I,i)) - (PartDiffSeq (g,Z,I,i)) by VFUNCT_1:25 ;
:: thesis: verum