let X be BCI-algebra; :: thesis: for x, y being Element of X
for n being Element of NAT holds x,(x \ (x \ y)) to_power n = x,y to_power n
let x, y be Element of X; :: thesis: for n being Element of NAT holds x,(x \ (x \ y)) to_power n = x,y to_power n
let n be Element of NAT ; :: thesis: x,(x \ (x \ y)) to_power n = x,y to_power n
defpred S₁[ set ] means for m being Element of NAT st m = $1 & m <= n holds
x,(x \ (x \ y)) to_power m = x,y to_power m;

now

let k be Element of NAT ; :: thesis: ( ( for m being Element of NAT st m = k & m <= n holds
x,(x \ (x \ y)) to_power m = x,y to_power m ) implies for m being Element of NAT st m = k + 1 & m <= n holds
x,(x \ (x \ y)) to_power (k + 1) = x,y to_power (k + 1) )
assume A1: for m being Element of NAT st m = k & m <= n holds
x,(x \ (x \ y)) to_power m = x,y to_power m ; :: thesis: for m being Element of NAT st m = k + 1 & m <= n holds
x,(x \ (x \ y)) to_power (k + 1) = x,y to_power (k + 1)
let m be Element of NAT ; :: thesis: ( m = k + 1 & m <= n implies x,(x \ (x \ y)) to_power (k + 1) = x,y to_power (k + 1) )
A2: x,(x \ (x \ y)) to_power (k + 1) = (x,(x \ (x \ y)) to_power k) \ (x \ (x \ y)) by Th4;
assume ( m = k + 1 & m <= n ) ; :: thesis: x,(x \ (x \ y)) to_power (k + 1) = x,y to_power (k + 1)
then k <= n by NAT_1:13;
hence x,(x \ (x \ y)) to_power (k + 1) = (x,y to_power k) \ (x \ (x \ y)) by A1, A2
.= (x \ (x \ (x \ y))),y to_power k by Th7
.= (x \ y),y to_power k by BCIALG_1:8
.= (x,y to_power k) \ y by Th7
.= x,y to_power (k + 1) by Th4 ;
:: thesis: verum

end;

then A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1] ;
x,(x \ (x \ y)) to_power 0 = x by Th1;
then A4: S₁[ 0 ] by Th1;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A3);
hence x,(x \ (x \ y)) to_power n = x,y to_power n ; :: thesis: verum