theorem Th63: :: RING_3:64

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)