reconsider g = p gcd q as Element of (Polynom-Ring F) ;
( p = 0. (Polynom-Ring F) & q = 0. (Polynom-Ring F) ) by STRUCT_0:def 12;
then ( p = 0_. F & q = 0_. F ) by POLYNOM3:def 10;
hence p gcd q is zero ; :: thesis: verum