let m, n be 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 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 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 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 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:9;
then m - n >= 1 by NAT_1:14;
then (m - n) + n >= 1 + n by XREAL_1:6;
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 Nat st k >= n holds
(x,y) to_power n = (x,y) to_power k

proof

let k be 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₁[ Nat] means ( $1 <= k1 implies (x,y) to_power n = (((x,y) to_power n),y) to_power $1 );

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

let k be 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 Nat st S₁[k] holds
S₁[k + 1] ;
A9: S₁[ 0 ] by BCIALG_2:1;
for n being Nat holds S₁[n] from NAT_1:sch 2(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 Nat st k >= n holds
(x,y) to_power n = (x,y) to_power k ; :: thesis: verum