let R be gcdDomain; :: thesis: for a being Element of R
for g being a_gcd of a, 0. R holds g is_associated_to a
let a be Element of R; :: thesis: for g being a_gcd of a, 0. R holds g is_associated_to a
let g be a_gcd of a, 0. R; :: thesis: g is_associated_to a
a is a_gcd of a, 0. R by lemgcd0a;
hence g is_associated_to a by RING_4:49; :: thesis: verum