consider a being Element of R such that
A: a is_a_root_of p by POLYNOM5:def 8;
thus p *' q is with_roots by A, prl2, POLYNOM5:def 8; :: thesis: verum