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 Th74; :: thesis: (f + g) `partial| (Z,I) = (f `partial| (Z,I)) + (g `partial| (Z,I))
reconsider k = (len I) - 1 as Element of NAT by FINSEQ_1:20, INT_1:5;
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;
A4: (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, Th74
.= (((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1)))) + (((PartDiffSeq (g,Z,I)) . k) `partial| (Z,(I /. (k + 1)))) by A2, A1, A3, Th65 ;
(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