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
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 AS: ( 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₁[ Element of 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 ;
A9: 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 Q2: ( (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 AS, TDef6;
Q0: ( f = (PartDiffSeq (f,Z,I)) . Z0 & (PartDiffSeq ((f + g),Z,I)) . Z0 = f + g ) by TDef5;
1 <= len I by FINSEQ_1:20;
then I /. 1 in Seg m by AS, XCWLM1;
then ( 1 <= I /. 1 & I /. 1 <= m ) by FINSEQ_1:1;
then ((PartDiffSeq (f,Z,I)) . Z0) + ((PartDiffSeq (g,Z,I)) . Z0) is_partial_differentiable_on Z,I /. (Z0 + 1) by AS, Q2, XXX1;
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 Q0, TDef5; :: thesis: verum

end;

A7: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
assume A81: 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)) )
A83: k <= k + 1 by NAT_1:11;
then A82: k <= (len I) - 1 by A81, XXREAL_0:2;
A84: ( (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 A81, AS, TDef6;
k + 1 <= ((len I) - 1) + 1 by A82, XREAL_1:6;
then I /. (k + 1) in Seg m by AS, XCWLM1, NAT_1:11;
then Q4: ( 1 <= I /. (k + 1) & I /. (k + 1) <= m ) by FINSEQ_1:1;
A840: ( (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 A82, AS, TDef6;
R1: (PartDiffSeq (f,Z,I)) . (k + 1) = ((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1))) by TDef5;
(k + 1) + 1 <= ((len I) - 1) + 1 by A81, XREAL_1:6;
then I /. ((k + 1) + 1) in Seg m by AS, XCWLM1, NAT_1:11;
then Q5: ( 1 <= I /. ((k + 1) + 1) & I /. ((k + 1) + 1) <= m ) by FINSEQ_1:1;
A86: (PartDiffSeq ((f + g),Z,I)) . (k + 1) = (((PartDiffSeq (f,Z,I)) . k) + ((PartDiffSeq (g,Z,I)) . k)) `partial| (Z,(I /. (k + 1))) by A83, A8, A81, TDef5, XXREAL_0:2
.= (((PartDiffSeq (f,Z,I)) . k) `partial| (Z,(I /. (k + 1)))) + (((PartDiffSeq (g,Z,I)) . k) `partial| (Z,(I /. (k + 1)))) by A840, AS, Q4, XXX1
.= ((PartDiffSeq (f,Z,I)) . (k + 1)) + ((PartDiffSeq (g,Z,I)) . (k + 1)) by R1, TDef5 ;
hence (PartDiffSeq ((f + g),Z,I)) . (k + 1) is_partial_differentiable_on Z,I /. ((k + 1) + 1) by AS, A84, Q5, XXX1; :: 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 A86; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A9, A7);
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;