take rpoly (2,(0. R)) ; :: thesis: ( rpoly (2,(0. R)) is monic & rpoly (2,(0. R)) is quadratic )
thus ( rpoly (2,(0. R)) is monic & rpoly (2,(0. R)) is quadratic ) by HURWITZ:27; :: thesis: verum