let G be RealNormSpace-Sequence; :: thesis: for F being 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 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 = In (i0,(dom G));
assume A1: 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 A2: (f1 + f2) * (reproj ((In (i0,(dom G))),x)) = (f1 * (reproj ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x))) by Th26;
assume A3: ( 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)) )
hence f1 + f2 is_partial_differentiable_in x,i0 by A2, NDIFF_1:35; :: 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 ((In (i0,(dom G))),x))) + (f2 * (reproj ((In (i0,(dom G))),x)))),((proj (In (i0,(dom G)))) . x)) by A3, NDIFF_1:35
.= partdiff ((f1 + f2),x,i0) by A1, Th26 ; :: thesis: verum