len (unital_poly (L,n)) = n + 1 by Th40;
hence unital_poly (L,n) is non-zero by UPROOTS:17; :: thesis: verum