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

hence
not p *' q is with_roots
; :: thesis: verumassume
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 ;

end;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 ;