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)) ) )
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)) ) )
set i = modetrans (G,i0);
assume ( 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)) )
then A3: ( 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 Def9;
(f1 - f2) * (reproj ((modetrans (G,i0)),x)) = (f1 * (reproj ((modetrans (G,i0)),x))) - (f2 * (reproj ((modetrans (G,i0)),x))) by AS, Th26;
then (f1 - f2) * (reproj ((modetrans (G,i0)),x)) is_differentiable_in (proj (modetrans (G,i0))) . x by A3, NDIFF_1:36;
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 A3, NDIFF_1:36
.= partdiff ((f1 - f2),x,i0) by AS, Th26 ; :: thesis: verum