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

let p, q be Polynomial of L; :: thesis: (Roots p) \/ (Roots q) c= Roots (p *' q)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Roots p) \/ (Roots q) or x in Roots (p *' q) )

assume A1: x in (Roots p) \/ (Roots q) ; :: thesis: x in Roots (p *' q)

let p, q be Polynomial of L; :: thesis: (Roots p) \/ (Roots q) c= Roots (p *' q)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Roots p) \/ (Roots q) or x in Roots (p *' q) )

assume A1: x in (Roots p) \/ (Roots q) ; :: thesis: x in Roots (p *' q)

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

end;

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 A2, 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: verum

end;a is_a_root_of p by A2, 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: verum

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 A3, 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: verum

end;a is_a_root_of q by A3, 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: verum