for L being non empty right_zeroed addLoopStr
for a being Element of L holds 2 * a = a + a