let R be domRing; :: thesis: for B being bag of the carrier of R st card (support B) = 1 holds
ex p being Ppoly of R st
( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) )
let B be bag of the carrier of R; :: thesis: ( card (support B) = 1 implies ex p being Ppoly of R st
( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) ) )
assume card (support B) = 1 ; :: thesis: ex p being Ppoly of R st
( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) )
then consider x being object such that
A1: support B = {x} by CARD_2:42;
x in support B by A1, TARSKI:def 1;
then reconsider a = x as Element of the carrier of R ;
reconsider q = rpoly (1,a) as Element of (Polynom-Ring R) by POLYNOM3:def 10;
deffunc H₁( set ) -> Element of (Polynom-Ring R) = q;
consider F being FinSequence of (Polynom-Ring R) such that
A2: ( len F = B . a & ( for k being Nat st k in dom F holds
F . k = H₁(k) ) ) from FINSEQ_2:sch 1();
reconsider F = F as non empty FinSequence of (Polynom-Ring R) by A1, A2, bb7;
reconsider p = Product F as Polynomial of R by POLYNOM3:def 10;
AS: B = ({a},(B . a)) -bag by A1, bb7;
A3: for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) by A2;
then reconsider p = p as Ppoly of R by dpp1;
take p ; :: thesis: ( deg p = card B & ( for a being Element of R holds multiplicity (p,a) = B . a ) )
thus deg p = B . a by A2, A3, lemppoly
.= card B by AS, bb4 ; :: thesis: for a being Element of R holds multiplicity (p,a) = B . a
A5: (rpoly (1,a)) `^ (B . a) = p by lempolybag1, A2;

now :: thesis: for o being Element of R holds multiplicity (p,o) = B . o

let o be Element of R; :: thesis: multiplicity (p,b₁) = B . b₁

per cases ( o = a or o <> a ) ;

suppose C: o = a ; :: thesis: multiplicity (p,b₁) = B . b₁

(rpoly (1,a)) `^ (B . a) = ((rpoly (1,a)) `^ (B . a)) *' (1_. R) ;
then B: (rpoly (1,a)) `^ (B . a) divides p by A5, RING_4:1;
E: (rpoly (1,a)) `^ (B . a) <> 0_. R ;
(rpoly (1,a)) `^ ((B . a) + 1) = ((rpoly (1,a)) `^ (B . a)) *' (rpoly (1,a)) by POLYNOM5:19;
then deg ((rpoly (1,a)) `^ ((B . a) + 1)) = (deg ((rpoly (1,a)) `^ (B . a))) + (deg (rpoly (1,a))) by E, HURWITZ:23
.= (deg ((rpoly (1,a)) `^ (B . a))) + 1 by HURWITZ:27 ;
then deg ((rpoly (1,a)) `^ ((B . a) + 1)) > deg ((rpoly (1,a)) `^ (B . a)) by XREAL_1:29;
hence multiplicity (p,o) = B . o by C, B, A5, prl25, multip; :: thesis: verum

end;

suppose C: o <> a ; :: thesis: multiplicity (p,b₁) = B . b₁

then C1: not o in support B by A1, TARSKI:def 1;
(rpoly (1,o)) `^ 0 = 1_. R by POLYNOM5:15;
then B: ((rpoly (1,o)) `^ 0) *' p = p ;

now :: thesis: not (rpoly (1,o)) `^ (0 + 1) divides p

assume (rpoly (1,o)) `^ (0 + 1) divides p ; :: thesis: contradiction
then rpoly (1,o) divides p by POLYNOM5:16;
then eval (p,o) = 0. R by Th9;
then o is_a_root_of p by POLYNOM5:def 7;
then o in Roots p by POLYNOM5:def 10;
then o in {a} by lempolybag1, A2;
hence contradiction by C, TARSKI:def 1; :: thesis: verum

end;

hence multiplicity (p,o) = 0 by B, multip, RING_4:1
.= B . o by C1, PRE_POLY:def 7 ;
:: thesis: verum

end;

end;

end;

hence for a being Element of R holds multiplicity (p,a) = B . a ; :: thesis: verum