let L be domRing; :: thesis: for p, q being Polynomial of L holds Roots (p *' q) = (Roots p) \/ (Roots q)
let p, q be Polynomial of L; :: thesis: Roots (p *' q) = (Roots p) \/ (Roots q)

now

let x be set ; :: thesis: ( ( x in Roots (p *' q) implies x in (Roots p) \/ (Roots q) ) & ( x in (Roots p) \/ (Roots q) implies b₁ in Roots (p *' q) ) )

hereby :: thesis: ( x in (Roots p) \/ (Roots q) implies b₁ in Roots (p *' q) )

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

per cases ( eval p,a = 0. L or eval q,a = 0. L ) by A2, VECTSP_2:def 5;

suppose eval p,a = 0. L ; :: thesis: x in (Roots p) \/ (Roots q)

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

end;

suppose eval q,a = 0. L ; :: thesis: x in (Roots p) \/ (Roots q)

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

end;

end;

end;

assume A3: x in (Roots p) \/ (Roots q) ; :: thesis: b₁ in Roots (p *' q)

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

suppose A4: x in Roots p ; :: thesis: b₁ in Roots (p *' q)

then reconsider a = x as Element of L ;
a is_a_root_of p by A4, 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 A5: x in Roots q ; :: thesis: b₁ in Roots (p *' q)

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

end;

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