let x0, y0, z0 be Real; :: thesis: for a, p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st a = <*x0,y0,z0*> holds
Directiondiff f,p,a = ((((partdiff f,p,1) * x0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + (((partdiff f,p,2) * y0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) + (((partdiff f,p,3) * z0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))
let a, p be Element of REAL 3; :: thesis: for f being PartFunc of (REAL 3),REAL st a = <*x0,y0,z0*> holds
Directiondiff f,p,a = ((((partdiff f,p,1) * x0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + (((partdiff f,p,2) * y0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) + (((partdiff f,p,3) * z0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))
let f be PartFunc of (REAL 3),REAL ; :: thesis: ( a = <*x0,y0,z0*> implies Directiondiff f,p,a = ((((partdiff f,p,1) * x0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + (((partdiff f,p,2) * y0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) + (((partdiff f,p,3) * z0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) )
assume A1: a = <*x0,y0,z0*> ; :: thesis: Directiondiff f,p,a = ((((partdiff f,p,1) * x0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + (((partdiff f,p,2) * y0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) + (((partdiff f,p,3) * z0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))
then A3: sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )) = sqrt (((x0 ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )) by FINSEQ_1:62
.= sqrt (((x0 ^2 ) + (y0 ^2 )) + ((a . 3) ^2 )) by A1, FINSEQ_1:62
.= sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )) by A1, FINSEQ_1:62 ;
Directiondiff f,p,a = (((partdiff f,p,1) * ((a . 1) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) + ((partdiff f,p,2) * ((unitvector a) . 2))) + ((partdiff f,p,3) * ((unitvector a) . 3)) by FINSEQ_1:62
.= ((((partdiff f,p,1) * (a . 1)) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) + ((partdiff f,p,2) * ((unitvector a) . 2))) + ((partdiff f,p,3) * ((unitvector a) . 3)) by XCMPLX_1:75
.= ((((partdiff f,p,1) * (a . 1)) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) + ((partdiff f,p,2) * ((a . 2) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))))) + ((partdiff f,p,3) * ((unitvector a) . 3)) by FINSEQ_1:62
.= ((((partdiff f,p,1) * (a . 1)) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) + (((partdiff f,p,2) * (a . 2)) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) + ((partdiff f,p,3) * ((unitvector a) . 3)) by XCMPLX_1:75
.= ((((partdiff f,p,1) * (a . 1)) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) + (((partdiff f,p,2) * (a . 2)) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) + ((partdiff f,p,3) * ((a . 3) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) by FINSEQ_1:62
.= ((((partdiff f,p,1) * (a . 1)) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) + (((partdiff f,p,2) * (a . 2)) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) + (((partdiff f,p,3) * (a . 3)) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) by XCMPLX_1:75
.= ((((partdiff f,p,1) * x0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + (((partdiff f,p,2) * (a . 2)) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))) + (((partdiff f,p,3) * (a . 3)) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) by A1, A3, FINSEQ_1:62
.= ((((partdiff f,p,1) * x0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + (((partdiff f,p,2) * y0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) + (((partdiff f,p,3) * (a . 3)) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))) by A1, A3, FINSEQ_1:62
.= ((((partdiff f,p,1) * x0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + (((partdiff f,p,2) * y0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) + (((partdiff f,p,3) * z0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) by A1, A3, FINSEQ_1:62 ;
hence Directiondiff f,p,a = ((((partdiff f,p,1) * x0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + (((partdiff f,p,2) * y0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) + (((partdiff f,p,3) * z0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) ; :: thesis: verum