theorem Th15: :: QUOFIELD:15

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