let X be BCI-algebra; :: thesis: for x, y, z being Element of X
for n, m being Element of 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 Element of NAT holds (x,y to_power n),z to_power m = (x,z to_power m),y to_power n
let n, m be Element of 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 Element of 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

(x,y to_power 0 ),z to_power m = x,z to_power m by Th1;
hence (x,y to_power 0 ),z to_power m = (x,z to_power m),y to_power 0 by Th1; :: thesis: verum

end;

then A1: S₁[ 0 ] ;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

now

let k be Element of NAT ; :: thesis: ( ( for m1 being Element of 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 Element of 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 A3: for m1 being Element of 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 Element of 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 Element of 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 A3
.= (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;

hence for k being Element of NAT st S₁[k] holds
S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence (x,y to_power n),z to_power m = (x,z to_power m),y to_power n ; :: thesis: verum