for m, n being non zero Nat
for i being Nat
for f being PartFunc of (REAL m),(REAL n)
for Z being Subset of (REAL m) st Z is open & 1 <= i & i <= m holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f is_partial_differentiable_in x,i ) ) )