for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for k being Element of NAT holds
( (power L) . ((- (1_ L)),(2 * k)) = 1_ L & (power L) . ((- (1_ L)),((2 * k) + 1)) = - (1_ L) )