theorem Th34: :: PDIFF_4:34

for p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL holds grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]|