:: deftheorem Def7 defines qmult QUOFIELD:def 7 :
for I being non degenerated commutative domRing-like Ring
for u, v, b₄ being Element of Quot. I holds
( b₄ = qmult (u,v) iff for z being Element of Q. I holds
( z in b₄ iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) ) );