let m be non zero Element of NAT ; 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); 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 ; 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; ( 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 )
; ( 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; (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; verum