for n being non zero Nat ex K being Field ex p being Polynomial of K st
( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )