for m being non zero Nat
for f being PartFunc of (REAL-NS m),(REAL-NS 1)
for X being Subset of (REAL-NS m) st X is open 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 ( f is_differentiable_on X & f `| X is_continuous_on X ) )