let m, n be Element of NAT ; :: thesis: for X being BCK-algebra
for x, y being Element of X st m > n & x,y to_power n = x,y to_power m holds
for k being Element of NAT st k >= n holds
x,y to_power n = x,y to_power k
let X be BCK-algebra; :: thesis: for x, y being Element of X st m > n & x,y to_power n = x,y to_power m holds
for k being Element of NAT st k >= n holds
x,y to_power n = x,y to_power k
let x, y be Element of X; :: thesis: ( m > n & x,y to_power n = x,y to_power m implies for k being Element of NAT st k >= n holds
x,y to_power n = x,y to_power k )
assume that
A1: m > n and
A2: x,y to_power n = x,y to_power m ; :: thesis: for k being Element of NAT st k >= n holds
x,y to_power n = x,y to_power k
( m - n is Element of NAT & m - n > n - n ) by A1, NAT_1:21, XREAL_1:11;
then m - n >= 1 by NAT_1:14;
then (m - n) + n >= 1 + n by XREAL_1:8;
then A3: x,y to_power n <= x,y to_power (n + 1) by A2, Th5;
A4: x,y to_power (n + 1) <= x,y to_power n by Th3;
for k being Element of NAT st k >= n holds
x,y to_power n = x,y to_power k

proof

let k be Element of NAT ; :: thesis: ( k >= n implies x,y to_power n = x,y to_power k )
assume k >= n ; :: thesis: x,y to_power n = x,y to_power k
then k - n is Element of NAT by NAT_1:21;
then consider k1 being Element of NAT such that
A5: k1 = k - n ;
x,y to_power n = (x,y to_power n),y to_power k1

proof

defpred S₁[ Element of NAT ] means ( $1 <= k1 implies x,y to_power n = (x,y to_power n),y to_power $1 );

now

let k be Element of NAT ; :: thesis: ( ( k <= k1 implies x,y to_power n = (x,y to_power n),y to_power k ) & k + 1 <= k1 implies x,y to_power n = (x,y to_power n),y to_power (k + 1) )
assume A6: ( k <= k1 implies x,y to_power n = (x,y to_power n),y to_power k ) ; :: thesis: ( k + 1 <= k1 implies x,y to_power n = (x,y to_power n),y to_power (k + 1) )
set m = k + 1;
A7: (x,y to_power n),y to_power (k + 1) = ((x,y to_power n),y to_power k) \ y by BCIALG_2:4
.= ((x,y to_power n) \ y),y to_power k by BCIALG_2:7
.= (x,y to_power (n + 1)),y to_power k by BCIALG_2:4
.= (x,y to_power n),y to_power k by A4, A3, Th2 ;
assume k + 1 <= k1 ; :: thesis: x,y to_power n = (x,y to_power n),y to_power (k + 1)
hence x,y to_power n = (x,y to_power n),y to_power (k + 1) by A6, A7, NAT_1:13; :: thesis: verum

end;

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

end;

then x,y to_power n = x,y to_power (n + k1) by BCIALG_2:10;
hence x,y to_power n = x,y to_power k by A5; :: thesis: verum

end;

hence for k being Element of NAT st k >= n holds
x,y to_power n = x,y to_power k ; :: thesis: verum