theorem Th13: :: BINOM:13

for R being non empty right_zeroed addLoopStr
for a being Element of R holds 1 * a = a