theorem ass0: :: RING_2:22

for R being domRing
for c being non zero Element of R
for b, a, d being Element of R st a * b is_associated_to c * d & a is_associated_to c holds
b is_associated_to d