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 sequence of the carrier of X st
( (x,y) to_power 0 = f . 0 & f . 0 = x & ( for j being Nat st j < 0 holds
f . (j + 1) = (f . j) \ y ) ) by Def1;
hence (x,y) to_power 0 = x ; :: thesis: verum