theorem Th1: :: BINOM:1

for R being non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr
for a being Element of R holds (0. R) * a = 0. R