let p be Ppoly of R; :: thesis: ( not p is constant & p is monic & p is with_roots )

consider F being non empty FinSequence of (Polynom-Ring R) such that

H: ( p = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) ) by dpp1;

A0: len F >= 1 + 0 by NAT_1:13;

hence not p is constant by H, lemppoly; :: thesis: ( p is monic & p is with_roots )

thus p is monic by cc2; :: thesis: p is with_roots

consider G being FinSequence of (Polynom-Ring R), x being Element of (Polynom-Ring R) such that

A1: F = G ^ <*x*> by A0, FINSEQ_2:19;

A3: F . ((len G) + 1) = x by A1, FINSEQ_1:42;

A4: len F = (len G) + (len <*x*>) by A1, FINSEQ_1:22

.= (len G) + 1 by FINSEQ_1:40 ;

len F in Seg (len F) by FINSEQ_1:3;

then len F in dom F by FINSEQ_1:def 3;

then consider a being Element of R such that

A2: x = rpoly (1,a) by H, A3, A4;

reconsider q = Product G as Polynomial of R by POLYNOM3:def 10;

p = (Product G) * x by H, A1, GROUP_4:6

.= q *' (rpoly (1,a)) by A2, POLYNOM3:def 10 ;

hence p is with_roots ; :: thesis: verum

consider F being non empty FinSequence of (Polynom-Ring R) such that

H: ( p = Product F & ( for i being Nat st i in dom F holds

ex a being Element of R st F . i = rpoly (1,a) ) ) by dpp1;

A0: len F >= 1 + 0 by NAT_1:13;

hence not p is constant by H, lemppoly; :: thesis: ( p is monic & p is with_roots )

thus p is monic by cc2; :: thesis: p is with_roots

consider G being FinSequence of (Polynom-Ring R), x being Element of (Polynom-Ring R) such that

A1: F = G ^ <*x*> by A0, FINSEQ_2:19;

A3: F . ((len G) + 1) = x by A1, FINSEQ_1:42;

A4: len F = (len G) + (len <*x*>) by A1, FINSEQ_1:22

.= (len G) + 1 by FINSEQ_1:40 ;

len F in Seg (len F) by FINSEQ_1:3;

then len F in dom F by FINSEQ_1:def 3;

then consider a being Element of R such that

A2: x = rpoly (1,a) by H, A3, A4;

reconsider q = Product G as Polynomial of R by POLYNOM3:def 10;

p = (Product G) * x by H, A1, GROUP_4:6

.= q *' (rpoly (1,a)) by A2, POLYNOM3:def 10 ;

hence p is with_roots ; :: thesis: verum