now :: thesis: not a * p is with_roots

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