:: deftheorem defines pdiff1 PDIFF_3:def 1 :
for i being Element of NAT
for n being non zero Element of NAT
for f being PartFunc of (REAL n),REAL
for b₄ being Function of (REAL n),REAL holds
( b₄ = pdiff1 (f,i) iff for z being Element of REAL n holds b₄ . z = partdiff (f,z,i) );