theorem Th161: :: ZMODUL01:161

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