theorem Th9: :: GCD_1:9

for R being commutative domRing-like Ring
for a being Element of R st a <> 0. R holds
a / a = 1. R