let F be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F)
for q being non zero Element of the carrier of (Polynom-Ring F) st q divides p holds
p gcd q = NormPolynomial q
let p be Element of the carrier of (Polynom-Ring F); :: thesis: for q being non zero Element of the carrier of (Polynom-Ring F) st q divides p holds
p gcd q = NormPolynomial q
let q be non zero Element of the carrier of (Polynom-Ring F); :: thesis: ( q divides p implies p gcd q = NormPolynomial q )
assume AS: q divides p ; :: thesis: p gcd q = NormPolynomial q
set s = NormPolynomial q;
B: NormPolynomial q divides p by AS, RING_4:25;
q = q *' (1_. F) ;
then C: NormPolynomial q divides q by RING_4:25, RING_4:1;

now :: thesis: for r being Polynomial of F st r divides p & r divides q holds
r divides NormPolynomial q

let r be Polynomial of F; :: thesis: ( r divides p & r divides q implies r divides NormPolynomial q )
assume D: ( r divides p & r divides q ) ; :: thesis: r divides NormPolynomial q
r is Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
hence r divides NormPolynomial q by D, RING_4:26; :: thesis: verum

end;

hence p gcd q = NormPolynomial q by C, B, RING_4:53; :: thesis: verum