let p be Element of (Polynom-Ring F); :: thesis: ( not p is zero & p is constant implies p is unital )
assume AS: ( not p is zero & p is constant ) ; :: thesis: p is unital
then A: p <> 0_. F by POLYNOM3:def 10;
reconsider pp = p as Element of the carrier of (Polynom-Ring F) ;
not pp is zero by A, UPROOTS:def 5;
then deg pp = 0 by AS;
hence p is unital by T8; :: thesis: verum