reconsider p = rpoly (2,(0. F)) as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
take p ; :: thesis: ( not p is linear & not p is constant )
deg p = 2 by HURWITZ:27;
hence ( not p is linear & not p is constant ) by FIELD_5:def 1, RING_4:def 4; :: thesis: verum