let m be non empty Element of NAT ; :: thesis: for X being Subset of (REAL m)
for I being non empty FinSequence of NAT
for f, g being PartFunc of (REAL m),REAL st X is open & rng I c= Seg m & f is_partial_differentiable_on X,I & g is_partial_differentiable_on X,I holds
( f - g is_partial_differentiable_on X,I & (f - g) `partial| (X,I) = (f `partial| (X,I)) - (g `partial| (X,I)) )
let Z be Subset of (REAL m); :: thesis: for I being non empty FinSequence of NAT
for f, g being PartFunc of (REAL m),REAL st Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f - g is_partial_differentiable_on Z,I & (f - g) `partial| (Z,I) = (f `partial| (Z,I)) - (g `partial| (Z,I)) )
let I be non empty FinSequence of NAT ; :: thesis: for f, g being PartFunc of (REAL m),REAL st Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f - g is_partial_differentiable_on Z,I & (f - g) `partial| (Z,I) = (f `partial| (Z,I)) - (g `partial| (Z,I)) )
let f, g be PartFunc of (REAL m),REAL; :: thesis: ( Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I implies ( f - g is_partial_differentiable_on Z,I & (f - g) `partial| (Z,I) = (f `partial| (Z,I)) - (g `partial| (Z,I)) ) )
assume AS: ( Z is open & rng I c= Seg m & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I ) ; :: thesis: ( f - g is_partial_differentiable_on Z,I & (f - g) `partial| (Z,I) = (f `partial| (Z,I)) - (g `partial| (Z,I)) )
then for i being Element of NAT st i <= (len I) - 1 holds
(PartDiffSeq ((f - g),Z,I)) . i is_partial_differentiable_on Z,I /. (i + 1) by XCW020;
hence f - g is_partial_differentiable_on Z,I by TDef6; :: thesis: (f - g) `partial| (Z,I) = (f `partial| (Z,I)) - (g `partial| (Z,I))
1 <= len I by FINSEQ_1:20;
then reconsider k = (len I) - 1 as Element of NAT by INT_1:5;
P1: ( (PartDiffSeq (f,Z,I)) . k is_partial_differentiable_on Z,I /. (k + 1) & (PartDiffSeq (g,Z,I)) . k is_partial_differentiable_on Z,I /. (k + 1) ) by AS, TDef6;
1 <= k + 1 by NAT_1:11;
then I /. (k + 1) in Seg m by AS, XCWLM1;
then Q4: ( 1 <= I /. (k + 1) & I /. (k + 1) <= m ) by FINSEQ_1:1;
(PartDiffSeq ((f - g),Z,I)) . (k + 1) = ((PartDiffSeq ((f - g),Z,I)) . k) `partial| (Z,(I /. (k + 1))) by TDef5
.= (((PartDiffSeq (f,Z,I)) . k) - ((PartDiffSeq (g,Z,I)) . k)) `partial| (Z,(I /. (k + 1))) by AS, XCW020 ;
then R1: (PartDiffSeq ((f - g),Z,I)) . (k + 1) = (((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1)))) - (((PartDiffSeq (g,Z,I)) . k) `partial| (Z,(I /. (k + 1)))) by P1, AS, Q4, XXX2;
(PartDiffSeq (f,Z,I)) . (k + 1) = ((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1))) by TDef5;
hence (f - g) `partial| (Z,I) = (f `partial| (Z,I)) - (g `partial| (Z,I)) by R1, TDef5; :: thesis: verum