let m be non zero 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 A1: ( 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)) )
hence f - g is_partial_differentiable_on Z,I by Th76; :: thesis: (f - g) `partial| (Z,I) = (f `partial| (Z,I)) - (g `partial| (Z,I))
reconsider k = (len I) - 1 as Element of NAT by INT_1:5, FINSEQ_1:20;
A2: ( (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 A1;
1 <= k + 1 by NAT_1:11;
then I /. (k + 1) in Seg m by A1, Lm6;
then A3: ( 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 Def7
.= (((PartDiffSeq (f,Z,I)) . k) - ((PartDiffSeq (g,Z,I)) . k)) `partial| (Z,(I /. (k + 1))) by A1, Th76 ;
then A4: (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 A2, A1, A3, Th66;
(PartDiffSeq (f,Z,I)) . (k + 1) = ((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1))) by Def7;
hence (f - g) `partial| (Z,I) = (f `partial| (Z,I)) - (g `partial| (Z,I)) by A4, Def7; :: thesis: verum