theorem Th66: :: RING_3:67

for R being non empty right_complementable Abelian add-associative right_zeroed distributive left_unital doubleLoopStr
for i, j being Integer holds (i * j) '*' (1. R) = (i '*' (1. R)) * (j '*' (1. R))