now :: thesis: not a * p is with_roots

assume a * p is with_roots ; :: thesis: contradiction
then consider b being Element of R such that
A: b is_a_root_of a * p by POLYNOM5:def 8;
0. R = eval ((a * p),b) by A, POLYNOM5:def 7
.= a * (eval (p,b)) by Th30 ;
then eval (p,b) = 0. R by VECTSP_2:def 1;
hence contradiction by POLYNOM5:def 8, POLYNOM5:def 7; :: thesis: verum

end;

hence not a * p is with_roots ; :: thesis: verum