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