theorem Th29: :: POLYNOM5:29

for L being non empty right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr
for v being Element of L holds v * (1_. L) = <%v%>