for I being non degenerated commutative domRing-like Ring
for u, v being Element of Q. I st ex w being Element of Quot. I st
( u in w & v in w ) holds
(u `1) * (v `2) = (v `1) * (u `2)