theorem Th14: :: BINOM:14

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