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:24;

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

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:7;
then eval ((p *' q),a) = 0. L by POLYNOM4:24;
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:6;
then eval ((p *' q),a) = 0. L by POLYNOM4:24;
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:1; :: thesis: verum