let X be BCI-algebra; :: thesis: for x being Element of X holds x |^ (- 1) = x `
let x be Element of X; :: thesis: x |^ (- 1) = x `
x |^ (- 1) = (BCI-power X) . (x ` ),(abs (- 1)) by Def2;
then x |^ (- 1) = (BCI-power X) . (x ` ),(- (- 1)) by ABSVALUE:def 1;
then x |^ (- 1) = (x ` ) |^ 1 ;
hence x |^ (- 1) = x ` by Th3; :: thesis: verum