:: deftheorem Def15 defines quotmultinv QUOFIELD:def 15 :
for I being non degenerated commutative domRing-like Ring
for b₂ being UnOp of (Quot. I) holds
( b₂ = quotmultinv I iff for u being Element of Quot. I holds b₂ . u = qmultinv u );