deg (npoly (R,n)) = n by lem6;
hence not npoly (R,n) is zero by HURWITZ:20; :: thesis: verum