theorem Th23: :: QUOFIELD:23
for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of Quot. I holds (quotmult I) . (((quotmult I) . (u,v)),w) = (quotmult I) . (u,((quotmult I) . (v,w)))