let F be Field; :: thesis: for p, q being Element of the carrier of (Polynom-Ring F) st p,q are_coprime holds
p,q have_no_common_roots
let p, q be Element of the carrier of (Polynom-Ring F); :: thesis: ( p,q are_coprime implies p,q have_no_common_roots )
set P = Polynom-Ring F;
assume AS: p,q are_coprime ; :: thesis: p,q have_no_common_roots
Y: 1. (Polynom-Ring F) = 1_. F by POLYNOM3:def 10;

now :: thesis: not p,q have_a_common_root

assume p,q have_a_common_root ; :: thesis: contradiction
then consider a being Element of F such that
A: a is_a_common_root_of p,q by RATFUNC1:def 4;
B: ( a is_a_root_of p & a is_a_root_of q ) by A, RATFUNC1:def 3;
then consider rp being Polynomial of F such that
C: p = (rpoly (1,a)) *' rp by HURWITZ:33;
consider rq being Polynomial of F such that
D: q = (rpoly (1,a)) *' rq by B, HURWITZ:33;
reconsider rpa = rpoly (1,a) as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
( rpoly (1,a) divides p & rpoly (1,a) divides q ) by D, C, RING_4:1;
then rpa divides 1. (Polynom-Ring F) by AS, RING_4:def 10;
then rpoly (1,a) divides 1_. F by Y;
then deg (rpoly (1,a)) <= deg (1_. F) by RING_5:13;
then 1 <= deg (1_. F) by HURWITZ:27;
hence contradiction by RATFUNC1:def 2; :: thesis: verum

end;

hence p,q have_no_common_roots ; :: thesis: verum