reconsider p1 = p, q1 = q as Element of (Polynom-Ring F) ;
set g1 = p1 gcd q1;
set g = p gcd q;
reconsider g1 = p1 gcd q1 as Element of (Polynom-Ring F) ;

D: 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;
D3: q <> 0_. F ;
g1 divides q1 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, D3, POLYNOM3:def 10; :: thesis: verum

end;

hence not p gcd q is zero ; :: thesis: p gcd q is monic
p gcd q <> 0_. F by D;
hence p gcd q is monic by dpg; :: thesis: verum