theorem :: TAYLOR_1:22

for p, x0 being Real
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)) )