:: deftheorem defines grad PDIFF_4:def 7 :
for f being PartFunc of (REAL 3),REAL
for p being Element of REAL 3 holds grad (f,p) = (((partdiff (f,p,1)) * <e1>) + ((partdiff (f,p,2)) * <e2>)) + ((partdiff (f,p,3)) * <e3>);