theorem Lm1: :: VECTSP13:2

for R being non empty Abelian addLoopStr
for n being Nat
for u, v being Tuple of n, the carrier of R holds u + v = v + u