let G be non-trivial RealNormSpace-Sequence; :: thesis: for F being non trivial RealNormSpace
for f1, f2 being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G & f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )
let F be non trivial RealNormSpace; :: thesis: for f1, f2 being PartFunc of (product G),F
for x being Point of (product G)
for i being set st i in dom G & f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )
let f1, f2 be PartFunc of (product G),F; :: thesis: for x being Point of (product G)
for i being set st i in dom G & f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )
let x be Point of (product G); :: thesis: for i being set st i in dom G & f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 + f2 is_partial_differentiable_in x,i & partdiff ((f1 + f2),x,i) = (partdiff (f1,x,i)) + (partdiff (f2,x,i)) )
let i0 be set ; :: thesis: ( i0 in dom G & f1 is_partial_differentiable_in x,i0 & f2 is_partial_differentiable_in x,i0 implies ( f1 + f2 is_partial_differentiable_in x,i0 & partdiff ((f1 + f2),x,i0) = (partdiff (f1,x,i0)) + (partdiff (f2,x,i0)) ) )
set i = modetrans (G,i0);
assume AS: i0 in dom G ; :: thesis: ( not f1 is_partial_differentiable_in x,i0 or not f2 is_partial_differentiable_in x,i0 or ( f1 + f2 is_partial_differentiable_in x,i0 & partdiff ((f1 + f2),x,i0) = (partdiff (f1,x,i0)) + (partdiff (f2,x,i0)) ) )
then A0: (f1 + f2) * (reproj ((modetrans (G,i0)),x)) = (f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x))) by Th26;
assume A1: ( f1 is_partial_differentiable_in x,i0 & f2 is_partial_differentiable_in x,i0 ) ; :: thesis: ( f1 + f2 is_partial_differentiable_in x,i0 & partdiff ((f1 + f2),x,i0) = (partdiff (f1,x,i0)) + (partdiff (f2,x,i0)) )
A2: ( f1 * (reproj ((modetrans (G,i0)),x)) is_differentiable_in (proj (modetrans (G,i0))) . x & f2 * (reproj ((modetrans (G,i0)),x)) is_differentiable_in (proj (modetrans (G,i0))) . x ) by A1, Def9;
then (f1 + f2) * (reproj ((modetrans (G,i0)),x)) is_differentiable_in (proj (modetrans (G,i0))) . x by A0, NDIFF_1:35;
hence f1 + f2 is_partial_differentiable_in x,i0 by Def9; :: thesis: partdiff ((f1 + f2),x,i0) = (partdiff (f1,x,i0)) + (partdiff (f2,x,i0))
thus (partdiff (f1,x,i0)) + (partdiff (f2,x,i0)) = diff (((f1 * (reproj ((modetrans (G,i0)),x))) + (f2 * (reproj ((modetrans (G,i0)),x)))),((proj (modetrans (G,i0))) . x)) by A2, NDIFF_1:35
.= partdiff ((f1 + f2),x,i0) by AS, Th26 ; :: thesis: verum