deg (X^ (n,a)) = n by Lm12;
hence not X^ (n,a) is constant by RATFUNC1:def 2; :: thesis: X^ (n,a) is monic
LC (X^ (n,a)) = 1. R by Lm13;
hence X^ (n,a) is monic by RATFUNC1:def 7; :: thesis: verum