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 ,1,0 ]|)) + ((partdiff f,p,3) * |[0 ,0 ,1]|) 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 ,1]|) 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 Lm6
.= |[((partdiff f,p,1) + 0 ),((partdiff f,p,2) + 0 ),(0 + (partdiff f,p,3))]| by Lm6
.= |[(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