let L be non degenerated comRing; :: thesis: for p, q being Polynomial of L holds (Roots p) \/ (Roots q) c= Roots (p *' q)
let p, q be Polynomial of L; :: thesis: (Roots p) \/ (Roots q) c= Roots (p *' q)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Roots p) \/ (Roots q) or x in Roots (p *' q) )
assume A1: x in (Roots p) \/ (Roots q) ; :: thesis: x in Roots (p *' q)

per cases ( x in Roots p or x in Roots q ) by A1, XBOOLE_0:def 3;

suppose A2: x in Roots p ; :: thesis: x in Roots (p *' q)

then reconsider a = x as Element of L ;
a is_a_root_of p by A2, POLYNOM5:def 10;
then eval (p,a) = 0. L ;
then (eval (p,a)) * (eval (q,a)) = 0. L ;
then eval ((p *' q),a) = 0. L by POLYNOM4:24;
then a is_a_root_of p *' q ;
hence x in Roots (p *' q) by POLYNOM5:def 10; :: thesis: verum

end;

suppose A3: x in Roots q ; :: thesis: x in Roots (p *' q)

then reconsider a = x as Element of L ;
a is_a_root_of q by A3, POLYNOM5:def 10;
then eval (q,a) = 0. L ;
then (eval (p,a)) * (eval (q,a)) = 0. L ;
then eval ((p *' q),a) = 0. L by POLYNOM4:24;
then a is_a_root_of p *' q ;
hence x in Roots (p *' q) by POLYNOM5:def 10; :: thesis: verum

end;

end;