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 )
assume x in BCK-part X ; :: thesis: x |^ (- n) = 0. X
then consider y being Element of X such that
C3: ( y = x & 0. X <= y ) ;
defpred S₁[ Nat] means x |^ (- $1) = 0. X;
A1: S₁[ 0 ] by Def1;

A3: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[b₁ + 1] )
assume B1: S₁[n] ; :: thesis: S₁[b₁ + 1]
- (- (n + 1)) > 0 ;
then B3: - (n + 1) < 0 ;

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

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

then x |^ (- (n + 1)) = x ` by Th4
.= 0. X by C3, BCIALG_1:def 11 ;
hence S₁[n + 1] ; :: thesis: verum

end;

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

then (BCI-power X) . (x ` ),(abs (- n)) = 0. X by Def2, B1;
then (BCI-power X) . (x ` ),(- (- n)) = 0. X by BB, 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 C3, BCIALG_1:def 11;
then 0. X = (x ` ) |^ (n + 1) by Th1
.= (BCI-power X) . (x ` ),(- (- (n + 1)))
.= (BCI-power X) . (x ` ),(abs (- (n + 1))) by B3, ABSVALUE:def 1
.= x |^ (- (n + 1)) by Def2, B3 ;
hence S₁[n + 1] ; :: thesis: verum

end;

end;

end;

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