now :: thesis: for p, q being Element of the carrier of (Polynom-Ring F) holds p gcd q = q gcd p

let p, q be Element of the carrier of (Polynom-Ring F); :: thesis: b₁ gcd b₂ = b₂ gcd b₁

per cases ( ( p = 0_. F & q = 0_. F ) or p <> 0_. F or q <> 0_. F ) ;

suppose AS: ( p = 0_. F & q = 0_. F ) ; :: thesis: b₁ gcd b₂ = b₂ gcd b₁

thus p gcd q = q gcd p by AS; :: thesis: verum

end;

suppose AS: ( p <> 0_. F or q <> 0_. F ) ; :: thesis: b₁ gcd b₂ = b₂ gcd b₁

then ( p gcd q is a_gcd of p,q & p gcd q is monic ) by dpg;
hence p gcd q = q gcd p by AS, dpg; :: thesis: verum

end;

end;

end;

hence for p, q being Element of the carrier of (Polynom-Ring F) holds p gcd q = q gcd p ; :: thesis: verum