let X be BCI-algebra; :: thesis: for x, y being Element of X holds (x,y) to_power 1 = x \ y
let x, y be Element of X; :: thesis: (x,y) to_power 1 = x \ y
consider f being sequence of the carrier of X such that
A1: (x,y) to_power 1 = f . 1 and
A2: ( f . 0 = x & ( for j being Nat st j < 1 holds
f . (j + 1) = (f . j) \ y ) ) by Def1;
f . (0 + 1) = x \ y by A2, NAT_1:3;
hence (x,y) to_power 1 = x \ y by A1; :: thesis: verum