theorem Th2: :: TAYLOR_1:2

for n being Nat
for x being Real holds
( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) )