theorem LMPDIFF:
for
E,
F,
G being
RealNormSpace for
f being
PartFunc of
[:E,F:],
G for
Z being
Subset of
[:E,F:] for
z being
Point of
[:E,F:] st
Z is
open &
z in Z &
Z c= dom f holds
( (
f is_partial_differentiable_in`1 z implies (
f | Z is_partial_differentiable_in`1 z &
partdiff`1 (
f,
z)
= partdiff`1 (
(f | Z),
z) ) ) & (
f is_partial_differentiable_in`2 z implies (
f | Z is_partial_differentiable_in`2 z &
partdiff`2 (
f,
z)
= partdiff`2 (
(f | Z),
z) ) ) )