theorem
for
G being
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)) )