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

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