let L be domRing; :: thesis: for p, q being Polynomial of L holds Roots (p *' q) = () \/ ()
let p, q be Polynomial of L; :: thesis: Roots (p *' q) = () \/ ()
now :: thesis: for x being object holds
( ( x in Roots (p *' q) implies x in () \/ () ) & ( x in () \/ () implies x in Roots (p *' q) ) )
let x be object ; :: thesis: ( ( x in Roots (p *' q) implies x in () \/ () ) & ( x in () \/ () implies b1 in Roots (p *' q) ) )
hereby :: thesis: ( x in () \/ () implies b1 in Roots (p *' q) )
assume A1: x in Roots (p *' q) ; :: thesis: x in () \/ ()
then reconsider a = x as Element of L ;
a is_a_root_of p *' q by ;
then eval ((p *' q),a) = 0. L ;
then A2: (eval (p,a)) * (eval (q,a)) = 0. L by POLYNOM4:24;
end;
assume A3: x in () \/ () ; :: thesis: b1 in Roots (p *' q)
per cases ( x in Roots p or x in Roots q ) by ;
suppose A4: x in Roots p ; :: thesis: b1 in Roots (p *' q)
then reconsider a = x as Element of L ;
a is_a_root_of p by ;
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 A5: x in Roots q ; :: thesis: b1 in Roots (p *' q)
then reconsider a = x as Element of L ;
a is_a_root_of q by ;
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;
end;
hence Roots (p *' q) = () \/ () by TARSKI:2; :: thesis: verum