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 Th37
.= |[(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 Th37 ;
hence grad ((r (#) f),p) = r * (grad (f,p)) ; :: thesis: verum