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