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

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;

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;hence rpoly (k,a) is with_roots ; :: thesis: verum