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