let X be BCI-algebra; :: thesis: for x, y, z being Element of X
for n being Element of NAT holds ((x,y) to_power n) \ z = ((x \ z),y) to_power n
let x, y, z be Element of X; :: thesis: for n being Element of NAT holds ((x,y) to_power n) \ z = ((x \ z),y) to_power n
let n be Element of NAT ; :: thesis: ((x,y) to_power n) \ z = ((x \ z),y) to_power n
defpred S₁[ set ] means for m being Element of NAT st m = $1 & m <= n holds
((x,y) to_power m) \ z = ((x \ z),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,y) to_power m) \ z = ((x \ z),y) to_power m ) implies for m being Element of NAT st m = k + 1 & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1) )
assume A1: for m being Element of NAT st m = k & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power m ; :: thesis: for m being Element of NAT st m = k + 1 & m <= n holds
((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1)
let m be Element of NAT ; :: thesis: ( m = k + 1 & m <= n implies ((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1) )
assume that
A2: m = k + 1 and
A3: m <= n ; :: thesis: ((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1)
((x,y) to_power m) \ z = (((x,y) to_power k) \ y) \ z by A2, Th4;
then A4: ((x,y) to_power m) \ z = (((x,y) to_power k) \ z) \ y by BCIALG_1:7;
k <= n by A2, A3, NAT_1:13;
then ((x,y) to_power m) \ z = (((x \ z),y) to_power k) \ y by A1, A4;
hence ((x,y) to_power m) \ z = ((x \ z),y) to_power (k + 1) by Th4; :: thesis: verum

end;

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