theorem :: FIELD_1:4

for n being Nat
for R being non degenerated Ring
for a being non zero Element of R holds deg (anpoly (a,n)) = n by Lm1;