let X be BCI-algebra; :: thesis: for x being Element of X
for n being Nat holds x |^ (- n) = ((x ` ) ` ) |^ (- n)
let x be Element of X; :: thesis: for n being Nat holds x |^ (- n) = ((x ` ) ` ) |^ (- n)
let n be Nat; :: thesis: x |^ (- n) = ((x ` ) ` ) |^ (- n)
defpred S₁[ Nat] means x |^ (- $1) = ((x ` ) ` ) |^ (- $1);

A1: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
set m = - (n + 1);
- (- (n + 1)) > 0 ;
then A2: - (n + 1) < 0 ;
then x |^ (- (n + 1)) = (BCI-power X) . (x ` ),(abs (- (n + 1))) by Def2
.= (BCI-power X) . (((x ` ) ` ) ` ),(abs (- (n + 1))) by BCIALG_1:8
.= ((x ` ) ` ) |^ (- (n + 1)) by A2, Def2 ;
hence S₁[n + 1] ; :: thesis: verum

end;

x |^ 0 = 0. X by Def1
.= ((x ` ) ` ) |^ 0 by Def1 ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence x |^ (- n) = ((x ` ) ` ) |^ (- n) ; :: thesis: verum