let X be BCI-algebra; :: thesis: for x, y being Element of X holds x,y to_power 0 = x
let x, y be Element of X; :: thesis: x,y to_power 0 = x
ex f being Function of NAT ,the carrier of X st
( x,y to_power 0 = f . 0 & f . 0 = x & ( for j being Element of NAT st j < 0 holds
f . (j + 1) = (f . j) \ y ) ) by Def1;
hence x,y to_power 0 = x ; :: thesis: verum