let F be Field; :: thesis: for p being non constant monic Polynomial of F
for a being Element of F st (rpoly (1,a)) *' p is Ppoly of F holds
p is Ppoly of F
let p be non constant monic Polynomial of F; :: thesis: for a being Element of F st (rpoly (1,a)) *' p is Ppoly of F holds
p is Ppoly of F
let a be Element of F; :: thesis: ( (rpoly (1,a)) *' p is Ppoly of F implies p is Ppoly of F )
assume (rpoly (1,a)) *' p is Ppoly of F ; :: thesis: p is Ppoly of F
then consider G being non empty FinSequence of the carrier of (Polynom-Ring F) such that
A1: ( (rpoly (1,a)) *' p = Product G & ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) ) by RING_5:def 4;
eval ((rpoly (1,a)),a) = a - a by HURWITZ:29
.= 0. F by RLVECT_1:15 ;
then 0. F = (eval ((rpoly (1,a)),a)) * (eval (p,a))
.= eval (((rpoly (1,a)) *' p),a) by POLYNOM4:24 ;
then consider i being Nat such that
A2: ( i in dom G & G . i = rpoly (1,a) ) by A1, RATFUNC1:12;
set H = Del (G,i);
consider m being Nat such that
A3: ( len G = m + 1 & len (Del (G,i)) = m ) by A2, FINSEQ_3:104;
A4: ( rpoly (1,a) <> 0_. F & p <> 0_. F ) ;

now :: thesis: not Del (G,i) is empty

assume Del (G,i) is empty ; :: thesis: contradiction
then 1 = deg ((rpoly (1,a)) *' p) by A1, A3, lemppoly
.= (deg (rpoly (1,a))) + (deg p) by A4, HURWITZ:23
.= 1 + (deg p) by HURWITZ:27 ;
hence contradiction by RATFUNC1:def 2; :: thesis: verum

end;

then reconsider H = Del (G,i) as non empty FinSequence of the carrier of (Polynom-Ring F) by FINSEQ_3:105;
reconsider q = Product H as Polynomial of F by POLYNOM3:def 10;

now :: thesis: for j being Nat st j in dom H holds
ex b being Element of F st H . j = rpoly (1,b)

let j be Nat; :: thesis: ( j in dom H implies ex b being Element of F st H . b = rpoly (1,b₂) )
assume B1: j in dom H ; :: thesis: ex b being Element of F st H . b = rpoly (1,b₂)
B2: ( dom H = Seg m & dom G = Seg (m + 1) ) by A3, FINSEQ_1:def 3;
then dom H c= dom G by FINSEQ_1:5, NAT_1:11;
then consider b being Element of F such that
B3: G . j = rpoly (1,b) by A1, B1;
B4: ( 1 <= j & j <= m ) by B1, B2, FINSEQ_1:1;

per cases ( j < i or j >= i ) ;

suppose j < i ; :: thesis: ex b being Element of F st H . b = rpoly (1,b₂)

hence ex b being Element of F st H . j = rpoly (1,b) by B3, FINSEQ_3:110; :: thesis: verum

end;

suppose j >= i ; :: thesis: ex b being Element of F st H . b = rpoly (1,b₂)

then B5: H . j = G . (j + 1) by A2, A3, B4, FINSEQ_3:111;
( 1 <= j + 1 & j + 1 <= m + 1 ) by NAT_1:11, B4, XREAL_1:6;
then j + 1 in dom G by B2;
hence ex b being Element of F st H . j = rpoly (1,b) by A1, B5; :: thesis: verum

end;

end;

end;

then reconsider q = q as Ppoly of F by RING_5:def 4;
A4: G /. i = rpoly (1,a) by A2, PARTFUN1:def 6;
(rpoly (1,a)) *' p = (G /. i) * (Product H) by A1, A2, RATFUNC1:3
.= (rpoly (1,a)) *' q by A4, POLYNOM3:def 10 ;
hence p is Ppoly of F by RATFUNC1:7; :: thesis: verum