LC (p *' q) = (LC p) * (LC q) by NIVEN:46
.= (LC p) * (1. R) by RATFUNC1:def 7
.= (1. R) * (1. R) by RATFUNC1:def 7 ;
hence p *' q is monic ; :: thesis: verum