let R be domRing; :: thesis: for a being Element of R holds multiplicity ((rpoly (1,a)),a) = 1
let a be Element of R; :: thesis: multiplicity ((rpoly (1,a)),a) = 1
set p = rpoly (1,a);
(rpoly (1,a)) *' (1_. R) = rpoly (1,a) ;
then rpoly (1,a) divides rpoly (1,a) by RING_4:1;
then A: (rpoly (1,a)) `^ 1 divides rpoly (1,a) by POLYNOM5:16;
rpoly (1,a) <> 0_. R ;
then deg ((rpoly (1,a)) *' (rpoly (1,a))) = (deg (rpoly (1,a))) + (deg (rpoly (1,a))) by HURWITZ:23
.= (deg (rpoly (1,a))) + 1 by HURWITZ:27
.= 1 + 1 by HURWITZ:27 ;
then deg ((rpoly (1,a)) *' (rpoly (1,a))) > 1 ;
then B: deg ((rpoly (1,a)) *' (rpoly (1,a))) > deg (rpoly (1,a)) by HURWITZ:27;
(rpoly (1,a)) *' (rpoly (1,a)) = (rpoly (1,a)) `^ 2 by POLYNOM5:17;
then not (rpoly (1,a)) `^ (1 + 1) divides rpoly (1,a) by B, prl25;
hence multiplicity ((rpoly (1,a)),a) = 1 by A, multip; :: thesis: verum