for I being non degenerated commutative domRing-like Ring
for u being Element of (the_Field_of_Quotients I) st u <> 0. (the_Field_of_Quotients I) holds
ex v being Element of (the_Field_of_Quotients I) st u * v = 1. (the_Field_of_Quotients I)