let a be Element of the carrier of (Polynom-Ring F); :: thesis: ( a is unital implies ( not a is zero & a is constant ) )
reconsider p = a as Element of (Polynom-Ring F) ;
assume AS: a is unital ; :: thesis: ( not a is zero & a is constant )
then deg a = 0 by T88;
then a <> 0_. F by HURWITZ:20;
hence not a is zero by UPROOTS:def 5; :: thesis: a is constant
thus a is constant by AS; :: thesis: verum