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