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

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