reconsider g = p gcd q as Element of (Polynom-Ring F) ;
( g divides p & g divides q ) by A, dpg;
hence p gcd q is p,q -gcd by A, dpg; :: thesis: verum

set g = p gcd q;
reconsider p1 = p, q1 = q as Element of (Polynom-Ring F) ;
set g1 = p1 gcd q1;
reconsider g1 = p1 gcd q1 as Element of (Polynom-Ring F) ;
thus p gcd q is p,q -gcd by A, dpg; :: thesis: verum