let F be Field; :: thesis: for p being monic Polynomial of F
for r being Polynomial of F st p *' r is monic holds
r is monic
let p be monic Polynomial of F; :: thesis: for r being Polynomial of F st p *' r is monic holds
r is monic
let r be Polynomial of F; :: thesis: ( p *' r is monic implies r is monic )
assume p *' r is monic ; :: thesis: r is monic
then 1. F = LC (p *' r) by RATFUNC1:def 7
.= (LC p) * (LC r) by NIVEN:46
.= (1. F) * (LC r) by RATFUNC1:def 7 ;
hence r is monic by RATFUNC1:def 7; :: thesis: verum