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

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