for R being non empty addLoopStr
for a being Element of R
for i being Integer st i = 0 holds
(Int-mult-left R) . (i,a) = 0. R