:: deftheorem Def8 defines diff PDIFF_1:def 8 :
for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
for b₅ being Function of (REAL m),(REAL n) holds
( b₅ = diff (f,x) 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₅ = diff (g,y) ) );