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: b1 gcd b2 = b2 gcd b1
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: b1 gcd b2 = b2 gcd b1
thus p gcd q = q gcd p by AS; :: thesis: verum
end;
suppose AS: ( p <> 0_. F or q <> 0_. F ) ; :: thesis: b1 gcd b2 = b2 gcd b1
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