:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 13 :
for m, n being non zero Nat
for i being Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m holds
( f is_partial_differentiable_in x,i iff ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & g is_partial_differentiable_in y,i ) );