reconsider a = p, b = q as Element of (Polynom-Ring F) by POLYNOM3:def 10;
A0: p gcd q = a gcd b by dd;
q <> 0_. F ;
then q <> 0. (Polynom-Ring F) by POLYNOM3:def 10;
then reconsider b = b as non zero Element of (Polynom-Ring F) by STRUCT_0:def 12;
thus not p gcd q is zero by A0; :: thesis: p gcd q is monic
thus p gcd q is monic by A0; :: thesis: verum