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