theorem Th27: :: NIVEN:29

for L being non empty right_zeroed addLoopStr
for z0, z1 being Element of L holds <%z0%> + <%z1%> = <%(z0 + z1)%>