let F be domRing; :: thesis: for p, q being Polynomial of F st q divides p holds
Roots q c= Roots p
let p, q be Polynomial of F; :: thesis: ( q divides p implies Roots q c= Roots p )
assume q divides p ; :: thesis: Roots q c= Roots p
then consider u being Polynomial of F such that
AS: p = q *' u by RING_4:1;

now :: thesis: for o being object st o in Roots q holds
o in Roots p

let o be object ; :: thesis: ( o in Roots q implies o in Roots p )
assume A: o in Roots q ; :: thesis: o in Roots p
then reconsider a = o as Element of F ;
B: a is_a_root_of q by A, POLYNOM5:def 10;
eval (p,a) = (eval (q,a)) * (eval (u,a)) by AS, POLYNOM4:24
.= (0. F) * (eval (u,a)) by B, POLYNOM5:def 7 ;
then a is_a_root_of p by POLYNOM5:def 7;
hence o in Roots p by POLYNOM5:def 10; :: thesis: verum

end;

hence Roots q c= Roots p ; :: thesis: verum