let R be domRing; :: thesis: for p being Element of the carrier of (Polynom-Ring R)
for n being non zero Element of NAT holds (Deriv R) . (p |^ n) = n * ((p |^ (n - 1)) * ((Deriv R) . p))
let p be Element of the carrier of (Polynom-Ring R); :: thesis: for n being non zero Element of NAT holds (Deriv R) . (p |^ n) = n * ((p |^ (n - 1)) * ((Deriv R) . p))
let n be non zero Element of NAT ; :: thesis: (Deriv R) . (p |^ n) = n * ((p |^ (n - 1)) * ((Deriv R) . p))
reconsider n1 = n - 1 as Nat ;
(Deriv R) . (p |^ (n1 + 1)) = (n1 + 1) * ((p |^ n1) * ((Deriv R) . p)) by RINGDER1:7;
hence (Deriv R) . (p |^ n) = n * ((p |^ (n - 1)) * ((Deriv R) . p)) ; :: thesis: verum