theorem :: FIELD_15:51

for R being non degenerated commutative Ring
for n being non trivial Nat
for a being Element of R holds (Deriv R) . (X^ (n,a)) = n * (X^ ((n - 1),(0. R)))