let n be Nat; :: thesis: for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ n = 0. X
let X be BCI-Algebra_with_Condition(S); :: thesis: (0. X) |^ n = 0. X
defpred S₁[ set ] means for m being Nat st m = $1 & m <= n holds
(0. X) |^ m = 0. X;
A1: for k being Nat st S₁[k] holds
S₁[k + 1] by Lm6;
A2: S₁[ 0 ] by Def6;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1);
hence (0. X) |^ n = 0. X ; :: thesis: verum