let x0, y0, z0 be Real; :: thesis: for p, a 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 p, a 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 A2: sqrt ((((a . 1) ^2) + ((a . 2) ^2)) + ((a . 3) ^2)) = sqrt (((x0 ^2) + ((a . 2) ^2)) + ((a . 3) ^2)) by FINSEQ_1:45
.= sqrt (((x0 ^2) + (y0 ^2)) + ((a . 3) ^2)) by A1, FINSEQ_1:45
.= sqrt (((x0 ^2) + (y0 ^2)) + (z0 ^2)) by A1, FINSEQ_1:45 ;
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:45
.= ((((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:74
.= ((((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:45
.= ((((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:74
.= ((((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:45
.= ((((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:74
.= ((((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, A2, FINSEQ_1:45
.= ((((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, A2, FINSEQ_1:45
.= ((((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, A2, FINSEQ_1:45 ;
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