:: deftheorem Def7 defines diff NDIFF_4:def 7 :
for n being non zero Element of NAT
for f being PartFunc of (REAL-NS n),REAL
for x being Point of (REAL-NS n)
for b₄ being Function of (REAL-NS n),REAL holds
( b₄ = diff (f,x) iff ex g being PartFunc of (REAL n),REAL ex y being Element of REAL n st
( f = g & x = y & b₄ = diff (g,y) ) );