let S be RealNormSpace-Sequence; :: thesis: for T being RealNormSpace
for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f, g being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f + g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i)) ) )
let T be RealNormSpace; :: thesis: for Z being Subset of (product S)
for I being non empty FinSequence of dom S
for f, g being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f + g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i)) ) )
let Z be Subset of (product S); :: thesis: for I being non empty FinSequence of dom S
for f, g being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f + g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i)) ) )
let I be non empty FinSequence of dom S; :: thesis: for f, g being PartFunc of (product S),T st Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I holds
( f + g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i)) ) )
let f, g be PartFunc of (product S),T; :: thesis: ( Z is open & f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I implies ( f + g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i)) ) ) )
assume that
A1: Z is open and
A2: f is_partial_differentiable_on Z,I and
A3: g is_partial_differentiable_on Z,I ; :: thesis: ( f + g is_partial_differentiable_on Z,I & ( for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i)) ) )
1 <= len I by FINSEQ_1:20;
then 1 in dom I by FINSEQ_3:25;
then A6: I . 1 in rng I by FUNCT_1:3;
A8: f `partial| (Z,(I . 1)) = PartDiffSeq (f,Z,I,1) by Th13;
A9: g `partial| (Z,(I . 1)) = PartDiffSeq (g,Z,I,1) by Th13;
A10: Partdiff_SP (S,T,I,1) = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . 1),(dom S)))),T) by Th12;
A11: PartDiffSeq ((f + g),Z,I,1) = (f + g) `partial| (Z,(I . 1)) by Th13
.= (PartDiffSeq (f,Z,I,1)) + (PartDiffSeq (g,Z,I,1)) by A1, A2, A3, A6, A8, A9, A10, Th21 ;
defpred S₁[ Nat] means ( 1 <= $1 & $1 < len I implies ( PartDiffSeq ((f + g),Z,I,$1) is_partial_differentiable_on Z,I . ($1 + 1) & PartDiffSeq ((f + g),Z,I,($1 + 1)) = (PartDiffSeq (f,Z,I,($1 + 1))) + (PartDiffSeq (g,Z,I,($1 + 1))) ) );
A12: S₁[ 0 ] ;
A13: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A14: S₁[k] ; :: thesis: S₁[k + 1]
assume A15: ( 1 <= k + 1 & k + 1 < len I ) ; :: thesis: ( PartDiffSeq ((f + g),Z,I,(k + 1)) is_partial_differentiable_on Z,I . ((k + 1) + 1) & PartDiffSeq ((f + g),Z,I,((k + 1) + 1)) = (PartDiffSeq (f,Z,I,((k + 1) + 1))) + (PartDiffSeq (g,Z,I,((k + 1) + 1))) )
then A16: PartDiffSeq (f,Z,I,(k + 1)) is_partial_differentiable_on Z,I . ((k + 1) + 1) by A2;
A17: PartDiffSeq (g,Z,I,(k + 1)) is_partial_differentiable_on Z,I . ((k + 1) + 1) by A3, A15;
( 1 <= (k + 1) + 1 & (k + 1) + 1 <= len I ) by A15, NAT_1:13;
then (k + 1) + 1 in dom I by FINSEQ_3:25;
then A18: I . ((k + 1) + 1) in rng I by FUNCT_1:3;
then A19: ( (PartDiffSeq (f,Z,I,(k + 1))) + (PartDiffSeq (g,Z,I,(k + 1))) is_partial_differentiable_on Z,I . ((k + 1) + 1) & ((PartDiffSeq (f,Z,I,(k + 1))) + (PartDiffSeq (g,Z,I,(k + 1)))) `partial| (Z,(I . ((k + 1) + 1))) = ((PartDiffSeq (f,Z,I,(k + 1))) `partial| (Z,(I . ((k + 1) + 1)))) + ((PartDiffSeq (g,Z,I,(k + 1))) `partial| (Z,(I . ((k + 1) + 1)))) ) by A1, A16, A17, Th21;
A20: Partdiff_SP (S,T,I,((k + 1) + 1)) = R_NormSpace_of_BoundedLinearOperators ((S . (In ((I . ((k + 1) + 1)),(dom S)))),(Partdiff_SP (S,T,I,(k + 1)))) by A15, Th12;
A21: (PartDiffSeq (f,Z,I,(k + 1))) `partial| (Z,(I . ((k + 1) + 1))) = PartDiffSeq (f,Z,I,((k + 1) + 1)) by A15, Th13;
A23: ((PartDiffSeq (f,Z,I,(k + 1))) + (PartDiffSeq (g,Z,I,(k + 1)))) `partial| (Z,(I . ((k + 1) + 1))) = (PartDiffSeq (f,Z,I,((k + 1) + 1))) + (PartDiffSeq (g,Z,I,((k + 1) + 1))) by A15, A19, A20, A21, Th13;

per cases ( k = 0 or k <> 0 ) ;

suppose A24: k = 0 ; :: thesis: ( PartDiffSeq ((f + g),Z,I,(k + 1)) is_partial_differentiable_on Z,I . ((k + 1) + 1) & PartDiffSeq ((f + g),Z,I,((k + 1) + 1)) = (PartDiffSeq (f,Z,I,((k + 1) + 1))) + (PartDiffSeq (g,Z,I,((k + 1) + 1))) )

hence PartDiffSeq ((f + g),Z,I,(k + 1)) is_partial_differentiable_on Z,I . ((k + 1) + 1) by A1, A11, A16, A17, A18, Th21; :: thesis: PartDiffSeq ((f + g),Z,I,((k + 1) + 1)) = (PartDiffSeq (f,Z,I,((k + 1) + 1))) + (PartDiffSeq (g,Z,I,((k + 1) + 1)))
thus PartDiffSeq ((f + g),Z,I,((k + 1) + 1)) = (PartDiffSeq (f,Z,I,((k + 1) + 1))) + (PartDiffSeq (g,Z,I,((k + 1) + 1))) by A11, A15, A23, A24, Th13; :: thesis: verum

end;

suppose A26: k <> 0 ; :: thesis: ( PartDiffSeq ((f + g),Z,I,(k + 1)) is_partial_differentiable_on Z,I . ((k + 1) + 1) & PartDiffSeq ((f + g),Z,I,((k + 1) + 1)) = (PartDiffSeq (f,Z,I,((k + 1) + 1))) + (PartDiffSeq (g,Z,I,((k + 1) + 1))) )

hence PartDiffSeq ((f + g),Z,I,(k + 1)) is_partial_differentiable_on Z,I . ((k + 1) + 1) by A1, A14, A15, A16, A17, A18, Th21, NAT_1:13, NAT_1:14; :: thesis: PartDiffSeq ((f + g),Z,I,((k + 1) + 1)) = (PartDiffSeq (f,Z,I,((k + 1) + 1))) + (PartDiffSeq (g,Z,I,((k + 1) + 1)))
thus PartDiffSeq ((f + g),Z,I,((k + 1) + 1)) = (PartDiffSeq (f,Z,I,((k + 1) + 1))) + (PartDiffSeq (g,Z,I,((k + 1) + 1))) by A14, A15, A23, A26, Th13, NAT_1:13, NAT_1:14; :: thesis: verum

end;

end;

end;

A27: for k being Nat holds S₁[k] from NAT_1:sch 2(A12, A13);
hence f + g is_partial_differentiable_on Z,I by A1, A2, A3, A6, Th21; :: thesis: for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i))
thus for i being Nat st 1 <= i & i <= len I holds
PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i)) :: thesis: verum

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len I implies PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i)) )
assume A28: ( 1 <= i & i <= len I ) ; :: thesis: PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i))

per cases ( i = 1 or i <> 1 ) ;

suppose i = 1 ; :: thesis: PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i))

hence PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i)) by A11; :: thesis: verum

end;

suppose i <> 1 ; :: thesis: PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i))

then 1 < i by XXREAL_0:1, A28;
then 1 + 1 <= i by NAT_1:13;
then A29: 2 - 1 <= i - 1 by XREAL_1:9;
then i - 1 in NAT by INT_1:3;
then reconsider j = i - 1 as Nat ;
j < j + 1 by NAT_1:16;
then j < len I by A28, XXREAL_0:2;
then PartDiffSeq ((f + g),Z,I,(j + 1)) = (PartDiffSeq (f,Z,I,(j + 1))) + (PartDiffSeq (g,Z,I,(j + 1))) by A27, A29;
hence PartDiffSeq ((f + g),Z,I,i) = (PartDiffSeq (f,Z,I,i)) + (PartDiffSeq (g,Z,I,i)) ; :: thesis: verum

end;

end;

end;