theorem Th155: :: ZMODUL01:155

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