:: deftheorem Def14 defines quotaddinv QUOFIELD:def 14 :
for I being non degenerated commutative domRing-like Ring
for b₂ being UnOp of (Quot. I) holds
( b₂ = quotaddinv I iff for u being Element of Quot. I holds b₂ . u = qaddinv u );