:: deftheorem Def14 defines partdiff PDIFF_1:def 14 :
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 st f is_partial_differentiable_in x,i holds
for b₆ being Element of REAL n holds
( b₆ = partdiff (f,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 & b₆ = (partdiff (g,y,i)) . <*1*> ) );