let G be RealNormSpace-Sequence; 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; 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; 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); 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 ; ( 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 A1:
i0 in dom G
; ( 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 = In (i0,(dom G));
assume A2:
( f1 is_partial_differentiable_in x,i0 & f2 is_partial_differentiable_in x,i0 )
; ( f1 - f2 is_partial_differentiable_in x,i0 & partdiff ((f1 - f2),x,i0) = (partdiff (f1,x,i0)) - (partdiff (f2,x,i0)) )
(f1 - f2) * (reproj ((In (i0,(dom G))),x)) = (f1 * (reproj ((In (i0,(dom G))),x))) - (f2 * (reproj ((In (i0,(dom G))),x)))
by A1, Th26;
hence
f1 - f2 is_partial_differentiable_in x,i0
by A2, NDIFF_1:36; 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 A2, NDIFF_1:36
.=
partdiff ((f1 - f2),x,i0)
by A1, Th26
; verum