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

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),y to_power m = x,y to_power (m1 + m) ) implies for m1 being Element of NAT st m1 = k + 1 & m1 <= n holds
(x,y to_power m1),y to_power m = x,y to_power (m1 + m) )
assume A1: for m1 being Element of NAT st m1 = k & m1 <= n holds
(x,y to_power m1),y to_power m = x,y to_power (m1 + m) ; :: thesis: for m1 being Element of NAT st m1 = k + 1 & m1 <= n holds
(x,y to_power m1),y to_power m = x,y to_power (m1 + m)
let m1 be Element of NAT ; :: thesis: ( m1 = k + 1 & m1 <= n implies (x,y to_power m1),y to_power m = x,y to_power (m1 + m) )
assume that
A2: m1 = k + 1 and
A3: m1 <= n ; :: thesis: (x,y to_power m1),y to_power m = x,y to_power (m1 + m)
k <= n by A2, A3, NAT_1:13;
then (x,y to_power k),y to_power m = x,y to_power (k + m) by A1;
then ((x,y to_power k),y to_power m) \ y = x,y to_power ((k + m) + 1) by Th4;
then ((x,y to_power k) \ y),y to_power m = x,y to_power ((k + m) + 1) by Th7;
hence (x,y to_power m1),y to_power m = x,y to_power (m1 + m) by A2, Th4; :: thesis: verum

end;

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