reconsider q = a * p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
deg (a * p) = deg p by RING_5:4;
then deg q > 0 by RING_4:def 4;
hence a * p is non constant Element of the carrier of (Polynom-Ring F) by RING_4:def 4; :: thesis: verum