theorem Th15: :: GCD_1:15

for R being commutative domRing-like Ring
for a, b, c being Element of R st a <> 0. R & a * b divides a * c holds
b divides c