for n being Nat
for L being non empty right_zeroed addLoopStr
for x, y being Element of L holds (seq (n,x)) + (seq (n,y)) = seq (n,(x + y))