let L be non empty almost_left_invertible well-unital distributive associative commutative 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 Def2
.= x by BINOM:8 ; :: thesis: verum