let L be non degenerated comRing; :: thesis: for p, q being Polynomial of L holds () \/ () c= Roots (p *' q)
let p, q be Polynomial of L; :: thesis: () \/ () c= Roots (p *' q)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in () \/ () or x in Roots (p *' q) )
assume A1: x in () \/ () ; :: thesis: x in Roots (p *' q)
per cases ( x in Roots p or x in Roots q ) by ;
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 ;
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 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 ;
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;