theorem Th14: :: POLYNOM8:14

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