theorem Th16: :: QUOFIELD:16

for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of Quot. I holds qmult (u,(qadd (v,w))) = qadd ((qmult (u,v)),(qmult (u,w)))