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_{1}[ Nat] means ( $1 <= n implies ((0. X),x) to_power $1 = 0. X );

_{1}[k] holds

S_{1}[k + 1]
;

A3: S_{1}[ 0 ]
by BCIALG_2:1;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A3, A2);

hence ((0. X),x) to_power n = 0. X ; :: thesis: verum

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

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

then A2:
for k being Nat st S((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;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

S

A3: S

for n being Nat holds S

hence ((0. X),x) to_power n = 0. X ; :: thesis: verum