let n be Element of 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₁[ Element of NAT ] means ( $1 <= n implies (0. X),x to_power $1 = 0. X );
A1: S₁[ 0 ] by BCIALG_2:1;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

now

let k be Element of 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 A3: ( 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 A3, 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;

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 (0. X),x to_power n = 0. X ; :: thesis: verum