for n being Nat
for X being BCI-Algebra_with_Condition(S) holds (0. X) |^ n = 0. X