( p = 0_. F & q = 0_. F ) by UPROOTS:def 5;
then ( p = 0. (Polynom-Ring F) & q = 0. (Polynom-Ring F) ) by POLYNOM3:def 10;
then reconsider a = p, b = q as zero Element of (Polynom-Ring F) ;
p gcd q = a gcd b by dd;
hence p gcd q is zero ; :: thesis: verum