theorem :: PDIFF_4:42

for p, a being Element of REAL 3
for f being PartFunc of (REAL 3),REAL holds Directiondiff (f,p,a) = |((grad (f,p)),(unitvector a))|