theorem LM200: :: NDIFF_7:34

for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for f being PartFunc of [:X,Y:],W holds
( ( f is_partial_differentiable_in`1 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,1 implies f is_partial_differentiable_in`1 z ) & ( f is_partial_differentiable_in`2 z implies f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 ) & ( f * ((IsoCPNrSP (X,Y)) ") is_partial_differentiable_in (IsoCPNrSP (X,Y)) . z,2 implies f is_partial_differentiable_in`2 z ) )