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