theorem Th61: :: RING_3:62

for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for a being Element of R
for i, j being Integer holds (i + j) '*' a = (i '*' a) + (j '*' a)