let p be Element of the carrier of (Polynom-Ring F); :: thesis: ( not p is zero & p is constant implies p is unital )
assume ( not p is zero & p is constant ) ; :: thesis: p is unital
then deg p = 0 ;
hence p is unital by T8; :: thesis: verum