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 `),|.(- 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 Th4; :: thesis: verum