theorem Th24: :: PDIFF_9:24

for m, n being non zero Element of NAT
for f being PartFunc of (REAL m),(REAL n)
for g being PartFunc of (REAL-NS m),(REAL-NS n)
for X being Subset of (REAL m)
for Y being Subset of (REAL-NS m) st X = Y & X is open & f = g holds
( ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) iff ( g is_differentiable_on Y & g `| Y is_continuous_on Y ) )