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