theorem :: TAYLOR_1:3

for n being Nat
for x0 being Real
for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) )