for L being non empty right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr
for p being sequence of L holds p *' (1_. L) = p