:: deftheorem Def11 defines qmultinv QUOFIELD:def 11 :
for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I st u <> q0. I holds
for b₃ being Element of Quot. I holds
( b₃ = qmultinv u iff for z being Element of Q. I holds
( z in b₃ iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) );