let X be BCI-Algebra_with_Condition(S); :: thesis: for x being Element of X holds x |^ 2 = x * x

let x be Element of X; :: thesis: x |^ 2 = x * x

thus x |^ 2 = x |^ (1 + 1)

.= (x |^ 1) * x by Def6

.= x * x by Th21 ; :: thesis: verum

let x be Element of X; :: thesis: x |^ 2 = x * x

thus x |^ 2 = x |^ (1 + 1)

.= (x |^ 1) * x by Def6

.= x * x by Th21 ; :: thesis: verum