( deg (anpoly (a,n)) = n & n <> - 1 ) by Lm1;
hence not anpoly (a,n) is zero by HURWITZ:20, UPROOTS:def 5; :: thesis: verum