for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for k being Element of NAT holds (power L) . ((- (1_ L)),k) <> 0. L