take 1_. R ; :: thesis: ( 1_. R is Element of the carrier of (Polynom-Ring R) & not 1_. R is zero )
thus ( 1_. R is Element of the carrier of (Polynom-Ring R) & not 1_. R is zero ) by POLYNOM3:def 10; :: thesis: verum