theorem Y0: :: FIELD_11:6

for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds
( LC p = 0. R iff p = 0_ (n,R) )