let F be algebraic-closed Field; :: thesis: for p being non constant Polynomial of F ex a being Element of F ex q being Ppoly of F, BRoots p st a * q = p
let p be non constant Polynomial of F; :: thesis: ex a being Element of F ex q being Ppoly of F, BRoots p st a * q = p
consider q being Ppoly of F, BRoots p, r being non with_roots Polynomial of F such that
A: ( p = q *' r & Roots q = Roots p ) by acf;
reconsider r1 = r as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
(len r) - 1 <= 1 - 1 by XREAL_1:9, POLYNOM5:def 9;
then r1 is constant by HURWITZ:def 2;
then consider a being Element of F such that
B: r1 = a | F by RING_4:20;
take a ; :: thesis: ex q being Ppoly of F, BRoots p st a * q = p
take q ; :: thesis: a * q = p
thus p = q *' (a * (1_. F)) by A, B, RING_4:16
.= a * (q *' (1_. F)) by RATFUNC1:6
.= a * q ; :: thesis: verum