theorem Th64: :: RING_3:65

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 '*' (j '*' a)