theorem Th4:
for
E,
G,
F being
RealNormSpace for
Z being
Subset of
[:E,F:] for
f being
PartFunc of
[:E,F:],
G for
z being
Point of
[:E,F:] st
f is_differentiable_in z holds
(
f is_partial_differentiable_in`1 z &
f is_partial_differentiable_in`2 z & ( for
dx being
Point of
E for
dy being
Point of
F holds
(diff (f,z)) . [dx,dy] = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy) ) )