let F be non degenerated comRing; :: thesis: for p, q being Polynomial of F holds Roots p c= Roots (p *' q)
let p, q be Polynomial of F; :: thesis: Roots p c= Roots (p *' q)

now :: thesis: for o being object st o in Roots p holds
o in Roots (p *' q)

let o be object ; :: thesis: ( o in Roots p implies o in Roots (p *' q) )
assume A: o in Roots p ; :: thesis: o in Roots (p *' q)
then reconsider a = o as Element of F ;
a is_a_root_of p by A, POLYNOM5:def 10;
then a is_a_root_of p *' q by ro1;
hence o in Roots (p *' q) by POLYNOM5:def 10; :: thesis: verum

end;

hence Roots p c= Roots (p *' q) ; :: thesis: verum