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_{1}( 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_{1}(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;

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

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

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

hence
for a being Element of R holds multiplicity (p,a) = B . a
; :: thesis: verumlet o be Element of R; :: thesis: multiplicity (p,b_{1}) = B . b_{1}

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

end;

suppose C:
o = a
; :: thesis: multiplicity (p,b_{1}) = B . b_{1}

(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;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

suppose C:
o <> a
; :: thesis: multiplicity (p,b_{1}) = B . b_{1}

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 ;

.= B . o by C1, PRE_POLY:def 7 ;

:: thesis: verum

end;(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

hence multiplicity (p,o) =
0
by B, multip, RING_4:1
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;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

.= B . o by C1, PRE_POLY:def 7 ;

:: thesis: verum