theorem :: PDIFF_4:40

for p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st f is total & f is constant holds
grad (f,p) = 0.REAL 3