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