let X be BCI-Algebra_with_Condition(S); :: thesis: for x being Element of X holds x |^ 1 = x
let x be Element of X; :: thesis: x |^ 1 = x
thus x |^ 1 = x |^ (0 + 1)
.= (x |^ 0) * x by Def6
.= (0. X) * x by Def6
.= x by Th8 ; :: thesis: verum