set p = rpoly (1,x);
1 = deg (rpoly (1,x)) by HURWITZ:27
.= (len (rpoly (1,x))) - 1 ;
then 1 + 1 = len (rpoly (1,x)) ;
then (len (rpoly (1,x))) -' 1 = 1 by NAT_D:34;
then LC (rpoly (1,x)) = 1. L by HURWITZ:25;
hence rpoly (1,x) is monic by RATFUNC1:def 7; :: thesis: verum