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