theorem Th13: :: QUOFIELD:13
for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of Quot. I holds
( qmult (u,(qmult (v,w))) = qmult ((qmult (u,v)),w) & qmult (u,v) = qmult (v,u) )