let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; :: thesis: for x being Element of L holds pow x,1 = x
let x be Element of L; :: thesis: pow x,1 = x
thus pow x,1 = x |^ 1 by Def3
.= x by BINOM:8 ; :: thesis: verum