let R be gcdDomain; :: thesis: for a being Element of R holds a is a_gcd of a, 0. R
let a be Element of R; :: thesis: a is a_gcd of a, 0. R
A: a divides a ;
a * (0. R) = 0. R ;
then B: a divides 0. R by GCD_1:def 1;
for r being Element of R st r divides a & r divides 0. R holds
r divides a ;
hence a is a_gcd of a, 0. R by A, B, RING_4:def 10; :: thesis: verum