theorem Th3: :: QUOFIELD:3

for I being non empty non degenerated Abelian add-associative associative commutative distributive domRing-like doubleLoopStr
for u, v, w being Element of Q. I holds padd (u,(padd (v,w))) = padd ((padd (u,v)),w)