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

now :: thesis: for k being Nat st ( for m1 being Nat st m1 = k & m1 <= n holds
(((x,y) to_power m1),z) to_power m = (((x,z) to_power m),y) to_power m1 ) holds
for m1 being Nat st m1 = k + 1 & m1 <= n holds
(((x,y) to_power (k + 1)),z) to_power m = (((x,z) to_power m),y) to_power (k + 1)

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

end;

then A2: for k being Nat st S₁[k] holds
S₁[k + 1] ;
(((x,y) to_power 0),z) to_power m = (x,z) to_power m by Th1;
then A3: S₁[ 0 ] by Th1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A2);
hence (((x,y) to_power n),z) to_power m = (((x,z) to_power m),y) to_power n ; :: thesis: verum