theorem Th29: :: HFDIFF_1:29

for x being Real
for n being Element of NAT st x <> 0 holds
( (#Z n) ^ is_differentiable_in x & diff (((#Z n) ^),x) = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2)) )