:: deftheorem Def12 defines quotadd QUOFIELD:def 12 :
for I being non degenerated commutative domRing-like Ring
for b₂ being BinOp of (Quot. I) holds
( b₂ = quotadd I iff for u, v being Element of Quot. I holds b₂ . (u,v) = qadd (u,v) );