theorem :: REALALG1:5

for R being degenerated Ring
for p being Polynomial of R holds { i where i is Nat : p . i <> 0. R } = {}