let n be Nat; :: thesis: for X being BCK-algebra
for x being Element of X holds ((0. X),x) to_power n = 0. X
let X be BCK-algebra; :: thesis: for x being Element of X holds ((0. X),x) to_power n = 0. X
let x be Element of X; :: thesis: ((0. X),x) to_power n = 0. X
defpred S₁[ Nat] means ( $1 <= n implies ((0. X),x) to_power $1 = 0. X );

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

let k be Nat; :: thesis: ( ( k <= n implies ((0. X),x) to_power k = 0. X ) & k + 1 <= n implies ((0. X),x) to_power (k + 1) = 0. X )
assume A1: ( k <= n implies ((0. X),x) to_power k = 0. X ) ; :: thesis: ( k + 1 <= n implies ((0. X),x) to_power (k + 1) = 0. X )
set m = k + 1;
assume k + 1 <= n ; :: thesis: ((0. X),x) to_power (k + 1) = 0. X
then ((0. X),x) to_power (k + 1) = x ` by A1, BCIALG_2:4, NAT_1:13
.= 0. X by BCIALG_1:def 8 ;
hence ((0. X),x) to_power (k + 1) = 0. X ; :: thesis: verum

end;

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