set g = p gcd q;
reconsider g1 = p gcd q as Element of (Polynom-Ring F) ;
q <> 0. (Polynom-Ring F) ;
then D3: q <> 0_. F by POLYNOM3:def 10;

now :: thesis: not p gcd q is zero

assume p gcd q is zero ; :: thesis: contradiction
then p gcd q = 0_. F by UPROOTS:def 5;
then D1: p gcd q = 0. (Polynom-Ring F) by POLYNOM3:def 10;
g1 divides q by defGCD;
then consider v being Element of the carrier of (Polynom-Ring F) such that
D4: g1 * v = q ;
thus contradiction by D1, D4; :: thesis: verum

end;

hence not p gcd q is zero ; :: thesis: p gcd q is monic
thus p gcd q is monic by D3, dpg; :: thesis: verum