reconsider p = X^ (n,a) as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
deg (X^ (n,a)) = n by Lm12;
then not p is constant by RING_4:def 4;
hence X^ (n,a) is monic non constant Element of the carrier of (Polynom-Ring R) ; :: thesis: verum