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 consider D being Element of R such that
A1: (0. R) * D = A by Def1;
thus A = 0. R by A1, VECTSP_1:39; :: thesis: verum