let R be domRing; for a being Element of R holds multiplicity ((rpoly (1,a)),a) = 1
let a be Element of R; 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; verum