let L be domRing; :: thesis:
let p, q be Polynomial of L; :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

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

per cases by A2, VECTSP_2:def 1;

suppose eval (p,a) = 0. L ; :: thesis:

then a is_a_root_of p ;
then a in Roots p by POLYNOM5:def 10;
hence x in (Roots p) \/ (Roots q) by XBOOLE_0:def 3; :: thesis:

end;

suppose eval (q,a) = 0. L ; :: thesis:

then a is_a_root_of q ;
then a in Roots q by POLYNOM5:def 10;
hence x in (Roots p) \/ (Roots q) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

assume A3: x in (Roots p) \/ (Roots q) ; :: thesis:

per cases by A3, XBOOLE_0:def 3;

suppose A4: x in Roots p ; :: thesis:

then reconsider a = x as Element of L ;
a is_a_root_of p by A4, 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:

end;

suppose A5: x in Roots q ; :: thesis:

then reconsider a = x as Element of L ;
a is_a_root_of q by A5, 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:

end;

end;

end;

hence Roots (p *' q) = (Roots p) \/ (Roots q) by TARSKI:2; :: thesis: