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

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