let F be Field; :: thesis: for p, q being Element of the carrier of (Polynom-Ring F) holds
( p,q are_coprime iff p gcd q = 1_. F )
let p, q be Element of the carrier of (Polynom-Ring F); :: thesis: ( p,q are_coprime iff p gcd q = 1_. F )
set P = Polynom-Ring F;
reconsider o = 0_. F, e = 1_. F as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
consider a, b being Element of (Polynom-Ring F) such that
H: ( a = p & b = q & p gcd q = a gcd b ) by RING_4:def 12;
Y: 1. (Polynom-Ring F) = 1_. F by POLYNOM3:def 10;

now :: thesis: ( p,q are_coprime implies p gcd q = 1_. F )

assume AS: p,q are_coprime ; :: thesis: p gcd q = 1_. F
then AS1: ( 1. (Polynom-Ring F) divides p & 1. (Polynom-Ring F) divides q & ( for r being Element of the carrier of (Polynom-Ring F) st r divides p & r divides q holds
r divides 1. (Polynom-Ring F) ) ) by RING_4:def 10;

now :: thesis: ( p = 0_. F implies not q = 0_. F )

assume ( p = 0_. F & q = 0_. F ) ; :: thesis: contradiction
then p gcd q = o by H, RING_4:def 11;
then ( o divides p & o divides q & ( for r being Element of the carrier of (Polynom-Ring F) st r divides p & r divides q holds
r divides o ) ) by H, RING_4:51;
then 0_. F divides 1_. F by AS1, Y;
then consider r2 being Polynomial of F such that
E: (0_. F) *' r2 = 1_. F by RING_4:1;
thus contradiction by E; :: thesis: verum

end;

hence p gcd q = 1_. F by H, AS, Y, RING_4:def 11; :: thesis: verum

end;

hence ( p,q are_coprime iff p gcd q = 1_. F ) by H, POLYNOM3:def 10; :: thesis: verum