:: deftheorem Def13 defines quotmult QUOFIELD:def 13 :
for I being non degenerated commutative domRing-like Ring
for b₂ being BinOp of (Quot. I) holds
( b₂ = quotmult I iff for u, v being Element of Quot. I holds b₂ . (u,v) = qmult (u,v) );