theorem Th20: :: QUOFIELD:20

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