theorem Th163: :: ZMODUL01:163

for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for a being Element of R
for i, j being Element of INT.Ring holds (Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))