:: deftheorem Def6 defines qadd QUOFIELD:def 6 :
for I being non degenerated commutative domRing-like Ring
for u, v, b₄ being Element of Quot. I holds
( b₄ = qadd (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 `2)) + ((b `1) * (a `2))) ) ) );