let F be Field; :: thesis: for p being Element of the carrier of (Polynom-Ring F) holds p gcd (0_. F) = NormPolynomial p
let p be Element of the carrier of (Polynom-Ring F); :: thesis: p gcd (0_. F) = NormPolynomial p
set s = NormPolynomial p;

per cases ( p is zero or not p is zero ) ;

suppose A0: p is zero ; :: thesis: p gcd (0_. F) = NormPolynomial p

then A1: p = 0_. F by UPROOTS:def 5;
thus p gcd (0_. F) = 0_. F by A0, UPROOTS:def 5
.= NormPolynomial p by A1, RING_4:22 ; :: thesis: verum

end;

suppose S: not p is zero ; :: thesis: p gcd (0_. F) = NormPolynomial p

p *' (1_. F) = p ;
then B: NormPolynomial p divides p by RING_4:25, RING_4:1;
0_. F = (NormPolynomial p) *' (0_. F) ;
then C: NormPolynomial p divides 0_. F by RING_4:1;

now :: thesis: for r being Polynomial of F st r divides 0_. F & r divides p holds
r divides NormPolynomial p

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

end;

hence p gcd (0_. F) = NormPolynomial p by S, C, B, RING_4:53; :: thesis: verum

end;

end;