let a be Element of the carrier of (Polynom-Ring F); :: thesis: ( not a is constant implies ( not a is zero & not a is unital ) )
assume AS: not a is constant ; :: thesis: ( not a is zero & not a is unital )

now :: thesis: not a = 0_. F

assume a = 0_. F ; :: thesis: contradiction
then len a = 0 by POLYNOM4:3;
hence contradiction by AS; :: thesis: verum

end;

hence not a is zero by UPROOTS:def 5; :: thesis: not a is unital
thus not a is unital by AS; :: thesis: verum