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 by Def3;
then ex D being Element of R st (0. R) * D = A by Def1;
hence A = 0. R by VECTSP_1:7; :: thesis: verum