let R be algebraic-closed Field; :: thesis: for p being non constant monic Polynomial of R holds p is Ppoly of R, BRoots p
let p be non constant monic Polynomial of R; :: thesis: p is Ppoly of R, BRoots p
consider a being Element of R, q being Ppoly of R, BRoots p such that
A: p = a * q by cc4;
1. R = LC p by RATFUNC1:def 7
.= a * (LC q) by A, RATFUNC1:18
.= a * (1. R) by cc2
.= a ;
hence p is Ppoly of R, BRoots p by A; :: thesis: verum