reconsider a = 1_. R as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
take a ; :: thesis: ( not a is zero & a is constant )
thus not a is zero ; :: thesis: a is constant
len (1_. R) = 1 by POLYNOM4:4;
hence a is constant ; :: thesis: verum