reconsider a = p, b = q as Element of (Polynom-Ring F) by POLYNOM3:def 10;
take a gcd b ; :: thesis: ex a, b being Element of (Polynom-Ring F) st
( a = p & b = q & a gcd b = a gcd b )
thus ex a, b being Element of (Polynom-Ring F) st
( a = p & b = q & a gcd b = a gcd b ) ; :: thesis: verum