for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for p, q, r being sequence of L holds (p *' q) *' r = p *' (q *' r)