per cases ;

suppose ( p = 0_. F & q = 0_. F ) ; :: thesis:

hence ( ( p = 0_. F & q = 0_. F implies ex b₁ being Element of the carrier of (Polynom-Ring F) st b₁ = 0_. F ) & ( ( not p = 0_. F or not q = 0_. F ) implies ex b₁ being Element of the carrier of (Polynom-Ring F) st
( b₁ is a_gcd of p,q & b₁ is monic ) ) ) ; :: thesis:

end;

suppose AS: ( p <> 0_. F or q <> 0_. F ) ; :: thesis:

reconsider g = the a_gcd of p,q as Element of the carrier of (Polynom-Ring F) ;
reconsider p1 = p, q1 = q as Element of (Polynom-Ring F) ;
set r = NormPolynomial g;
reconsider r1 = NormPolynomial g as Element of (Polynom-Ring F) ;

A: now :: thesis:

assume g is zero ; :: thesis:
then g = 0_. F by UPROOTS:def 5;
then D1: g = 0. (Polynom-Ring F) by POLYNOM3:def 10;
g divides p1 by defGCD;
then consider u being Element of the carrier of (Polynom-Ring F) such that
D2: g * u = p1 ;
g divides q1 by defGCD;
then consider v being Element of the carrier of (Polynom-Ring F) such that
D4: g * v = q1 ;
thus contradiction by D1, D4, D2, AS, POLYNOM3:def 10; :: thesis:

end;

g divides p1 by defGCD;
then g divides p ;
then F: NormPolynomial g divides p by np1;
g divides q1 by defGCD;
then g divides q ;
then B: NormPolynomial g divides q by np1;

now :: thesis:

let z be Element of (Polynom-Ring F); :: thesis:
reconsider z1 = z as Element of the carrier of (Polynom-Ring F) ;
assume ( z divides p & z divides q ) ; :: thesis:
then z divides g by defGCD;
then z1 divides g ;
then z1 divides NormPolynomial g by np2;
hence z divides r1 ; :: thesis:

end;

then r1 is p,q -gcd by B, F;
hence ( ( p = 0_. F & q = 0_. F implies ex b₁ being Element of the carrier of (Polynom-Ring F) st b₁ = 0_. F ) & ( ( not p = 0_. F or not q = 0_. F ) implies ex b₁ being Element of the carrier of (Polynom-Ring F) st
( b₁ is a_gcd of p,q & b₁ is monic ) ) ) by A; :: thesis:

end;

end;