let F be Field; :: thesis: for p, q being non zero Polynomial of F st ( for a being Element of F st a is_a_root_of p *' q holds
multiplicity ((p *' q),a) = 1 ) holds
(Roots p) /\ (Roots q) = {}
let p, q be non zero Polynomial of F; :: thesis: ( ( for a being Element of F st a is_a_root_of p *' q holds
multiplicity ((p *' q),a) = 1 ) implies (Roots p) /\ (Roots q) = {} )
assume AS: for a being Element of F st a is_a_root_of p *' q holds
multiplicity ((p *' q),a) = 1 ; :: thesis: (Roots p) /\ (Roots q) = {}
set a = the Element of (Roots p) /\ (Roots q);

now :: thesis: not (Roots p) /\ (Roots q) <> {}

assume (Roots p) /\ (Roots q) <> {} ; :: thesis: contradiction
then B: ( the Element of (Roots p) /\ (Roots q) in Roots p & the Element of (Roots p) /\ (Roots q) in Roots q ) by XBOOLE_0:def 4;
then reconsider a = the Element of (Roots p) /\ (Roots q) as Element of F ;
D: ( a is_a_root_of p & a is_a_root_of q ) by B, POLYNOM5:def 10;
then C: ( a is_a_root_of p *' q & multiplicity (p,a) >= 1 & multiplicity (q,a) >= 1 ) by ro1, UPROOTS:52;
multiplicity ((p *' q),a) = (multiplicity (p,a)) + (multiplicity (q,a)) by UPROOTS:55;
then multiplicity ((p *' q),a) >= 1 + 1 by C, XREAL_1:7;
then multiplicity ((p *' q),a) > 1 by NAT_1:13;
hence contradiction by AS, D, ro1; :: thesis: verum

end;

hence (Roots p) /\ (Roots q) = {} ; :: thesis: verum