for n being Nat
for R being domRing
for x being Element of (Polynom-Ring R) st x = anpoly ((1. R),1) holds
ex y being Element of (Polynom-Ring R) st
( y = anpoly ((1. R),n) & (Der1 R) . (x |^ (n + 1)) = (n + 1) * y )