let R be domRing; :: thesis: for B being bag of the carrier of R st card () = 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 () = 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 () = 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 ;
then reconsider a = x as Element of the carrier of R ;
reconsider q = rpoly (1,a) as Element of () by POLYNOM3:def 10;
deffunc H1( set ) -> Element of () = q;
consider F being FinSequence of () such that
A2: ( len F = B . a & ( for k being Nat st k in dom F holds
F . k = H1(k) ) ) from reconsider F = F as non empty FinSequence of () by A1, A2, bb7;
reconsider p = Product F as Polynomial of R by POLYNOM3:def 10;
AS: B = ({a},(B . a)) -bag by ;
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
.= card B by ; :: thesis: for a being Element of R holds multiplicity (p,a) = B . a
A5: (rpoly (1,a)) `^ (B . a) = p by ;
now :: thesis: for o being Element of R holds multiplicity (p,o) = B . o
let o be Element of R; :: thesis: multiplicity (p,b1) = B . b1
per cases ( o = a or o <> a ) ;
suppose C: o = a ; :: thesis: multiplicity (p,b1) = B . b1
(rpoly (1,a)) `^ (B . a) = ((rpoly (1,a)) `^ (B . a)) *' (1_. R) ;
then B: (rpoly (1,a)) `^ (B . a) divides p by ;
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
.= (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;
end;
end;
hence for a being Element of R holds multiplicity (p,a) = B . a ; :: thesis: verum