theorem :: FIELD_11:12

for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds
( (LM p) . (Lt p) = LC p & ( for b being bag of n st b <> Lt p holds
(LM p) . b = 0. R ) ) by lemY, W2;