let r be Real; :: thesis: for p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 holds
grad (r (#) f),p = r * (grad f,p)
let p be Element of REAL 3; :: thesis: for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 holds
grad (r (#) f),p = r * (grad f,p)
let f be PartFunc of (REAL 3),REAL ; :: thesis: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 implies grad (r (#) f),p = r * (grad f,p) )
assume A1: ( f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 ) ; :: thesis: grad (r (#) f),p = r * (grad f,p)
grad (r (#) f),p = |[(partdiff (r (#) f),p,1),(partdiff (r (#) f),p,2),(partdiff (r (#) f),p,3)]| by Th43
.= |[(r * (partdiff f,p,1)),(partdiff (r (#) f),p,2),(partdiff (r (#) f),p,3)]| by A1, PDIFF_1:33
.= |[(r * (partdiff f,p,1)),(r * (partdiff f,p,2)),(partdiff (r (#) f),p,3)]| by A1, PDIFF_1:33
.= |[(r * (partdiff f,p,1)),(r * (partdiff f,p,2)),(r * (partdiff f,p,3))]| by A1, PDIFF_1:33
.= r * |[(partdiff f,p,1),(partdiff f,p,2),(partdiff f,p,3)]| by EUCLID_8:59
.= r * (grad f,p) by Th43 ;
hence grad (r (#) f),p = r * (grad f,p) ; :: thesis: verum