let X be BCI-algebra; :: thesis: for x being Element of X
for n being Nat st x in BCK-part X holds
x |^ (- n) = 0. X
let x be Element of X; :: thesis: for n being Nat st x in BCK-part X holds
x |^ (- n) = 0. X
let n be Nat; :: thesis: ( x in BCK-part X implies x |^ (- n) = 0. X )
defpred S₁[ Nat] means x |^ (- $1) = 0. X;
assume x in BCK-part X ; :: thesis: x |^ (- n) = 0. X
then A1: ex y being Element of X st
( y = x & 0. X <= y ) ;

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[b₁ + 1] )
assume A3: S₁[n] ; :: thesis: S₁[b₁ + 1]

per cases ( - n = 0 or - n < 0 ) ;

suppose - n = 0 ; :: thesis: S₁[b₁ + 1]

then x |^ (- (n + 1)) = x ` by Th5
.= 0. X by A1 ;
hence S₁[n + 1] ; :: thesis: verum

end;

suppose A4: - n < 0 ; :: thesis: S₁[b₁ + 1]

then (BCI-power X) . ((x `),|.(- n).|) = 0. X by A3, Def2;
then (BCI-power X) . ((x `),(- (- n))) = 0. X by A4, ABSVALUE:def 1;
then (x `) \ (((x `) |^ n) `) = (x \ (0. X)) ` by BCIALG_1:9
.= x ` by BCIALG_1:2 ;
then (x `) \ (((x `) |^ n) `) = 0. X by A1;
then 0. X = (x `) |^ (n + 1) by Th2
.= (BCI-power X) . ((x `),(- (- (n + 1))))
.= (BCI-power X) . ((x `),|.(- (n + 1)).|) by ABSVALUE:def 1
.= x |^ (- (n + 1)) by Def2 ;
hence S₁[n + 1] ; :: thesis: verum

end;

end;

end;

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