for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for x being Element of L
for n being Element of NAT holds
( pow (x,(n + 1)) = (pow (x,n)) * x & pow (x,(n + 1)) = x * (pow (x,n)) )