reconsider p = rpoly (2,(0. R)) as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
take p ; :: thesis: ( p is monic & p is quadratic )
thus ( p is monic & p is quadratic ) by HURWITZ:27; :: thesis: verum