let x0, p be real number ; :: thesis: for f being PartFunc of REAL ,REAL st f is_differentiable_in x0 & f . x0 > 0 holds
( (#R p) * f is_differentiable_in x0 & diff ((#R p) * f),x0 = (p * ((f . x0) #R (p - 1))) * (diff f,x0) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_differentiable_in x0 & f . x0 > 0 implies ( (#R p) * f is_differentiable_in x0 & diff ((#R p) * f),x0 = (p * ((f . x0) #R (p - 1))) * (diff f,x0) ) )
assume that
A1: f is_differentiable_in x0 and
A2: f . x0 > 0 ; :: thesis: ( (#R p) * f is_differentiable_in x0 & diff ((#R p) * f),x0 = (p * ((f . x0) #R (p - 1))) * (diff f,x0) )
A3: x0 is Real by XREAL_0:def 1;
A4: #R p is_differentiable_in f . x0 by A2, Th21;
hence (#R p) * f is_differentiable_in x0 by A1, A3, FDIFF_2:13; :: thesis: diff ((#R p) * f),x0 = (p * ((f . x0) #R (p - 1))) * (diff f,x0)
thus diff ((#R p) * f),x0 = (diff (#R p),(f . x0)) * (diff f,x0) by A1, A4, A3, FDIFF_2:13
.= (p * ((f . x0) #R (p - 1))) * (diff f,x0) by A2, Th21 ; :: thesis: verum