:: deftheorem defines Directiondiff PDIFF_4:def 9 :
for f being PartFunc of (REAL 3),REAL
for p, a being Element of REAL 3 holds Directiondiff (f,p,a) = (((partdiff (f,p,1)) * ((unitvector a) . 1)) + ((partdiff (f,p,2)) * ((unitvector a) . 2))) + ((partdiff (f,p,3)) * ((unitvector a) . 3));