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 set ; :: 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 9;
then eval p,a = 0. L by POLYNOM5:def 6;
then (eval p,a) * (eval q,a) = 0. L by VECTSP_1:39;
then eval (p *' q),a = 0. L by POLYNOM4:27;
then a is_a_root_of p *' q by POLYNOM5:def 6;
hence x in Roots (p *' q) by POLYNOM5:def 9; :: 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 9;
then eval q,a = 0. L by POLYNOM5:def 6;
then (eval p,a) * (eval q,a) = 0. L by VECTSP_1:36;
then eval (p *' q),a = 0. L by POLYNOM4:27;
then a is_a_root_of p *' q by POLYNOM5:def 6;
hence x in Roots (p *' q) by POLYNOM5:def 9; :: thesis: verum

end;

end;