theorem :: RING_3:66

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