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