let p, a be Element of REAL 3; :: thesis: for f being PartFunc of (REAL 3),REAL holds Directiondiff (f,p,a) = |((grad (f,p)),(unitvector a))|
let f be PartFunc of (REAL 3),REAL; :: thesis: Directiondiff (f,p,a) = |((grad (f,p)),(unitvector a))|
set p0 = grad (f,p);
reconsider g1 = grad (f,p), g2 = unitvector a as FinSequence of REAL ;
A1: len g1 = len <*((grad (f,p)) . 1),((grad (f,p)) . 2),((grad (f,p)) . 3)*> by EUCLID_8:1
.= 3 by FINSEQ_1:45 ;
A2: len g2 = 3 by FINSEQ_1:45;
A3: grad (f,p) = |[(partdiff (f,p,1)),(partdiff (f,p,2)),(partdiff (f,p,3))]| by Th34;
|((grad (f,p)),(unitvector a))| = Sum <*((g1 . 1) * (g2 . 1)),((g1 . 2) * (g2 . 2)),((g1 . 3) * (g2 . 3))*> by A1, A2, EUCLID_5:28
.= ((((grad (f,p)) . 1) * (g2 . 1)) + (((grad (f,p)) . 2) * (g2 . 2))) + (((grad (f,p)) . 3) * (g2 . 3)) by RVSUM_1:78
.= (((partdiff (f,p,1)) * (g2 . 1)) + (((grad (f,p)) . 2) * (g2 . 2))) + (((grad (f,p)) . 3) * (g2 . 3)) by A3, FINSEQ_1:45
.= (((partdiff (f,p,1)) * (g2 . 1)) + ((partdiff (f,p,2)) * (g2 . 2))) + (((grad (f,p)) . 3) * (g2 . 3)) by A3, FINSEQ_1:45
.= Directiondiff (f,p,a) by A3, FINSEQ_1:45 ;
hence Directiondiff (f,p,a) = |((grad (f,p)),(unitvector a))| ; :: thesis: verum