theorem :: BINOM:12

for R being non empty addLoopStr
for a being Element of R holds
( 0 * a = 0. R & a * 0 = 0. R ) by Def3, Def4;