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

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