let p be Element of REAL 3; :: thesis: for f being PartFunc of (REAL 3),REAL holds grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]|
let f be PartFunc of (REAL 3),REAL; :: thesis: grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]|
grad (f,p) = (|[((partdiff (f,p,1)) * 1),((partdiff (f,p,1)) * 0),((partdiff (f,p,1)) * 0)]| + ((partdiff (f,p,2)) * |[0,jj,0]|)) + ((partdiff (f,p,3)) * |[0,0,jj]|) by EUCLID_8:59
.= (|[(partdiff (f,p,1)),0,0]| + |[((partdiff (f,p,2)) * 0),((partdiff (f,p,2)) * 1),((partdiff (f,p,2)) * 0)]|) + ((partdiff (f,p,3)) * |[0,0,jj]|) by EUCLID_8:59
.= (|[(partdiff (f,p,1)),0,0]| + |[0,(partdiff (f,p,2)),0]|) + |[((partdiff (f,p,3)) * 0),((partdiff (f,p,3)) * 0),((partdiff (f,p,3)) * 1)]| by EUCLID_8:59
.= |[((partdiff (f,p,1)) + 0),(0 + (partdiff (f,p,2))),(0 + 0)]| + |[0,0,(partdiff (f,p,3))]| by Lm4
.= |[((partdiff (f,p,1)) + 0),((partdiff (f,p,2)) + 0),(0 + (partdiff (f,p,3)))]| by Lm4
.= |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]| ;
hence grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]| ; :: thesis: verum