for L being non empty right_complementable add-associative right_zeroed distributive associative doubleLoopStr
for k being odd Element of NAT
for x being Element of L holds (power L) . ((- x),k) = - ((power L) . (x,k))