theorem :: PDIFF_4:41

for x0, y0, z0 being Real
for p, a being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st a = <*x0,y0,z0*> holds
Directiondiff (f,p,a) = ((((partdiff (f,p,1)) * x0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)))) + (((partdiff (f,p,2)) * y0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))) + (((partdiff (f,p,3)) * z0) / (sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2))))