now :: thesis: for p, q being Polynomial of F holds p gcd q = q gcd p

let p, q be Polynomial of F; :: thesis: p gcd q = q gcd p
reconsider a = p, b = q as Element of (Polynom-Ring F) by POLYNOM3:def 10;
thus p gcd q = a gcd b by dd
.= q gcd p by dd ; :: thesis: verum

end;

hence for p, q being Polynomial of F holds p gcd q = q gcd p ; :: thesis: verum