let a be Element of (Polynom-Ring R); :: thesis: ( not a is constant implies ( not a is zero & not a is unital ) )
reconsider p = a as Element of the carrier of (Polynom-Ring R) ;
assume AS: not a is constant ; :: thesis: ( not a is zero & not a is unital )
then A: deg p > 0 ;
now :: thesis: not a = 0. (Polynom-Ring R)
assume a = 0. (Polynom-Ring R) ; :: thesis: contradiction
then p = 0_. R by POLYNOM3:def 10;
then len p = 0 by POLYNOM4:3;
hence contradiction by A; :: thesis: verum
end;
hence not a is zero ; :: thesis: not a is unital
thus not a is unital by AS, T88; :: thesis: verum