for R being commutative domRing-like Ring
for a, b being Element of R holds
( a is_associated_to b iff ex c being Element of R st
( c is unital & a * c = b ) )