theorem Th21: :: TAYLOR_1:21

for p, x being Real st x > 0 holds
( #R p is_differentiable_in x & diff ((#R p),x) = p * (x #R (p - 1)) )