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