theorem Lm2: :: VECTSP13:3

for R being non empty add-associative addLoopStr
for n being Nat
for u, v, w being Tuple of n, the carrier of R holds (u + v) + w = u + (v + w)