set p = rpoly (k,a);
thus not rpoly (k,a) is constant by HURWITZ:27; :: thesis: ( rpoly (k,a) is monic & rpoly (k,a) is with_roots )
deg (rpoly (k,a)) >= 0 ;
then (len (rpoly (k,a))) - 1 >= 0 by HURWITZ:def 2;
then 0 + 1 <= ((len (rpoly (k,a))) - 1) + 1 by XREAL_1:6;
then A: (len (rpoly (k,a))) -' 1 = (len (rpoly (k,a))) - 1 by XREAL_1:233
.= deg (rpoly (k,a)) by HURWITZ:def 2 ;
LC (rpoly (k,a)) = (rpoly (k,a)) . k by A, HURWITZ:27
.= 1_ R by HURWITZ:25
.= 1. R ;
hence rpoly (k,a) is monic ; :: thesis: rpoly (k,a) is with_roots

per cases ( k = 1 or k > 1 ) by NAT_1:53;

suppose k = 1 ; :: thesis: rpoly (k,a) is with_roots

hence rpoly (k,a) is with_roots ; :: thesis: verum

end;

suppose k > 1 ; :: thesis: rpoly (k,a) is with_roots

then (rpoly (1,a)) *' (qpoly (k,a)) = rpoly (k,a) by HURWITZ:32;
hence rpoly (k,a) is with_roots ; :: thesis: verum

end;

end;