theorem Th45: :: NDIFF13:44

for E, F, G being RealNormSpace
for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G st f is_differentiable_on Z holds
( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & ( for z being Point of [:E,F:] st z in Z holds
( ( for dx being Point of E holds ((f `partial`1| Z) /. z) . dx = ((f `| Z) /. z) . (dx,(0. F)) ) & ( for dy being Point of F holds ((f `partial`2| Z) /. z) . dy = ((f `| Z) /. z) . ((0. E),dy) ) ) ) )