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_{1}[ set ] means for m being Nat st m = $1 & m <= n holds

(0. X) |^ m = 0. X;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
by Lm6;

A2: S_{1}[ 0 ]
by Def6;

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

hence (0. X) |^ n = 0. X ; :: thesis: verum

let X be BCI-Algebra_with_Condition(S); :: thesis: (0. X) |^ n = 0. X

defpred S

(0. X) |^ m = 0. X;

A1: for k being Nat st S

S

A2: S

for n being Nat holds S

hence (0. X) |^ n = 0. X ; :: thesis: verum