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