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;
set q0 = unitvector a;
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:62 ;
A2: len g2 = 3 by FINSEQ_1:62;
A3: grad f,p = |[(partdiff f,p,1),(partdiff f,p,2),(partdiff f,p,3)]| by Th43;
|((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:108
.= (((partdiff f,p,1) * (g2 . 1)) + (((grad f,p) . 2) * (g2 . 2))) + (((grad f,p) . 3) * (g2 . 3)) by A3, FINSEQ_1:62
.= (((partdiff f,p,1) * (g2 . 1)) + ((partdiff f,p,2) * (g2 . 2))) + (((grad f,p) . 3) * (g2 . 3)) by A3, FINSEQ_1:62
.= Directiondiff f,p,a by A3, FINSEQ_1:62 ;
hence Directiondiff f,p,a = |((grad f,p),(unitvector a))| ; :: thesis: verum