theorem Th2: :: BINOM:2

for R being non empty right_add-cancelable left_zeroed right-distributive doubleLoopStr
for a being Element of R holds a * (0. R) = 0. R