theorem lemlp0: :: REALALG1:6

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