let L be non empty almost_left_invertible well-unital distributive associative commutative 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 Def2

.= 1_ L by BINOM:8 ;

hence pow (x,0) = 1. L ; :: thesis: verum

let x be Element of L; :: thesis: pow (x,0) = 1. L

pow (x,0) = x |^ 0 by Def2

.= 1_ L by BINOM:8 ;

hence pow (x,0) = 1. L ; :: thesis: verum