:: deftheorem Def10 defines qaddinv QUOFIELD:def 10 :
for I being non degenerated commutative domRing-like Ring
for u, b₃ being Element of Quot. I holds
( b₃ = qaddinv 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 `2) = (z `2) * (- (a `1)) ) ) );