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 S1[ 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
.= 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 S1[k] holds
S1[k + 1] ;
A3: S1[ 0 ] by BCIALG_2:1;
for n being Nat holds S1[n] from NAT_1:sch 2(A3, A2);
hence ((0. X),x) to_power n = 0. X ; :: thesis: verum