let R be commutative domRing-like Ring; :: thesis: for a being Element of R st a is_associated_to 0. R holds
a = 0. R
let A be Element of R; :: thesis: ( A is_associated_to 0. R implies A = 0. R )
assume A is_associated_to 0. R ; :: thesis: A = 0. R
then 0. R divides A ;
then ex D being Element of R st (0. R) * D = A ;
hence A = 0. R ; :: thesis: verum