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