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