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
for i being Element of NAT st i <= (len I) - 1 holds
( (PartDiffSeq ((f + g),X,I)) . i is_partial_differentiable_on X,I /. (i + 1) & (PartDiffSeq ((f + g),X,I)) . i = ((PartDiffSeq (f,X,I)) . i) + ((PartDiffSeq (g,X,I)) . 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
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) & (PartDiffSeq ((f + g),Z,I)) . i = ((PartDiffSeq (f,Z,I)) . i) + ((PartDiffSeq (g,Z,I)) . 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
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) & (PartDiffSeq ((f + g),Z,I)) . i = ((PartDiffSeq (f,Z,I)) . i) + ((PartDiffSeq (g,Z,I)) . 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 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) & (PartDiffSeq ((f + g),Z,I)) . i = ((PartDiffSeq (f,Z,I)) . i) + ((PartDiffSeq (g,Z,I)) . 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: 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) & (PartDiffSeq ((f + g),Z,I)) . i = ((PartDiffSeq (f,Z,I)) . i) + ((PartDiffSeq (g,Z,I)) . i) )
thus 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) & (PartDiffSeq ((f + g),Z,I)) . i = ((PartDiffSeq (f,Z,I)) . i) + ((PartDiffSeq (g,Z,I)) . i) ) :: thesis: verum

proof

defpred S₁[ Nat] means ( $1 <= (len I) - 1 implies ( (PartDiffSeq ((f + g),Z,I)) . $1 is_partial_differentiable_on Z,I /. ($1 + 1) & (PartDiffSeq ((f + g),Z,I)) . $1 = ((PartDiffSeq (f,Z,I)) . $1) + ((PartDiffSeq (g,Z,I)) . $1) ) );
reconsider Z0 = 0 as Element of NAT ;
A2: S₁[ 0 ]

proof

assume 0 <= (len I) - 1 ; :: thesis: ( (PartDiffSeq ((f + g),Z,I)) . 0 is_partial_differentiable_on Z,I /. (0 + 1) & (PartDiffSeq ((f + g),Z,I)) . 0 = ((PartDiffSeq (f,Z,I)) . 0) + ((PartDiffSeq (g,Z,I)) . 0) )
then A3: ( (PartDiffSeq (f,Z,I)) . Z0 is_partial_differentiable_on Z,I /. (Z0 + 1) & (PartDiffSeq (g,Z,I)) . Z0 is_partial_differentiable_on Z,I /. (Z0 + 1) ) by A1;
A4: ( f | Z = (PartDiffSeq (f,Z,I)) . Z0 & g | Z = (PartDiffSeq (g,Z,I)) . Z0 & (PartDiffSeq ((f + g),Z,I)) . Z0 = (f + g) | Z ) by Def7;
A5: (f | Z) + (g | Z) = (f + g) | Z by RFUNCT_1:44;
1 <= len I by FINSEQ_1:20;
then I /. 1 in Seg m by A1, Lm6;
then ( 1 <= I /. 1 & I /. 1 <= m ) by FINSEQ_1:1;
hence ( (PartDiffSeq ((f + g),Z,I)) . 0 is_partial_differentiable_on Z,I /. (0 + 1) & (PartDiffSeq ((f + g),Z,I)) . 0 = ((PartDiffSeq (f,Z,I)) . 0) + ((PartDiffSeq (g,Z,I)) . 0) ) by A4, A5, A1, A3, Th65; :: thesis: verum

end;

A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
assume A8: k + 1 <= (len I) - 1 ; :: thesis: ( (PartDiffSeq ((f + g),Z,I)) . (k + 1) is_partial_differentiable_on Z,I /. ((k + 1) + 1) & (PartDiffSeq ((f + g),Z,I)) . (k + 1) = ((PartDiffSeq (f,Z,I)) . (k + 1)) + ((PartDiffSeq (g,Z,I)) . (k + 1)) )
A9: k <= k + 1 by NAT_1:11;
then A10: k <= (len I) - 1 by A8, XXREAL_0:2;
A11: ( (PartDiffSeq (f,Z,I)) . (k + 1) is_partial_differentiable_on Z,I /. ((k + 1) + 1) & (PartDiffSeq (g,Z,I)) . (k + 1) is_partial_differentiable_on Z,I /. ((k + 1) + 1) ) by A8, A1;
k + 1 <= ((len I) - 1) + 1 by A10, XREAL_1:6;
then I /. (k + 1) in Seg m by A1, Lm6, NAT_1:11;
then A12: ( 1 <= I /. (k + 1) & I /. (k + 1) <= m ) by FINSEQ_1:1;
k in NAT by ORDINAL1:def 12;
then A13: ( (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 A9, A1, A8, XXREAL_0:2;
A14: (PartDiffSeq (f,Z,I)) . (k + 1) = ((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1))) by Def7;
(k + 1) + 1 <= ((len I) - 1) + 1 by A8, XREAL_1:6;
then I /. ((k + 1) + 1) in Seg m by A1, Lm6, NAT_1:11;
then A15: ( 1 <= I /. ((k + 1) + 1) & I /. ((k + 1) + 1) <= m ) by FINSEQ_1:1;
A16: (PartDiffSeq ((f + g),Z,I)) . (k + 1) = (((PartDiffSeq (f,Z,I)) . k) + ((PartDiffSeq (g,Z,I)) . k)) `partial| (Z,(I /. (k + 1))) by A9, A7, A8, Def7, XXREAL_0:2
.= (((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1)))) + (((PartDiffSeq (g,Z,I)) . k) `partial| (Z,(I /. (k + 1)))) by A13, A1, A12, Th65
.= ((PartDiffSeq (f,Z,I)) . (k + 1)) + ((PartDiffSeq (g,Z,I)) . (k + 1)) by A14, Def7 ;
hence (PartDiffSeq ((f + g),Z,I)) . (k + 1) is_partial_differentiable_on Z,I /. ((k + 1) + 1) by A1, A11, A15, Th65; :: thesis: (PartDiffSeq ((f + g),Z,I)) . (k + 1) = ((PartDiffSeq (f,Z,I)) . (k + 1)) + ((PartDiffSeq (g,Z,I)) . (k + 1))
thus (PartDiffSeq ((f + g),Z,I)) . (k + 1) = ((PartDiffSeq (f,Z,I)) . (k + 1)) + ((PartDiffSeq (g,Z,I)) . (k + 1)) by A16; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A6);
hence 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) & (PartDiffSeq ((f + g),Z,I)) . i = ((PartDiffSeq (f,Z,I)) . i) + ((PartDiffSeq (g,Z,I)) . i) ) ; :: thesis: verum

end;