now :: thesis: not p *' q is with_roots

assume p *' q is with_roots ; :: thesis: contradiction
then consider a being Element of R such that
H: a is_a_root_of p *' q by POLYNOM5:def 8;
A: 0. R = eval ((p *' q),a) by H, POLYNOM5:def 7
.= (eval (p,a)) * (eval (q,a)) by POLYNOM4:24 ;

per cases ( eval (p,a) = 0. R or eval (q,a) = 0. R ) by A, VECTSP_2:def 1;

suppose eval (p,a) = 0. R ; :: thesis: contradiction

hence contradiction by POLYNOM5:def 8, POLYNOM5:def 7; :: thesis: verum

end;

suppose eval (q,a) = 0. R ; :: thesis: contradiction

hence contradiction by POLYNOM5:def 8, POLYNOM5:def 7; :: thesis: verum

end;

end;

end;

hence not p *' q is with_roots ; :: thesis: verum