let n be Nat; :: thesis: for R being non degenerated Ring
for a being non zero Element of R holds deg (anpoly (a,n)) = n
let R be non degenerated Ring; :: thesis: for a being non zero Element of R holds deg (anpoly (a,n)) = n
let a be non zero Element of R; :: thesis: deg (anpoly (a,n)) = n
len (anpoly (a,n)) = n + 1 by POLYDIFF:27;
hence deg (anpoly (a,n)) = n ; :: thesis: verum