let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for n being Nat holds (a `) |^ n = a |^ (- n)
let a be Element of AtomSet X; :: thesis: for n being Nat holds (a `) |^ n = a |^ (- n)
let n be Nat; :: thesis: (a `) |^ n = a |^ (- n)

per cases ( n = 0 or n > 0 ) ;

suppose A1: n = 0 ; :: thesis: (a `) |^ n = a |^ (- n)

hence (a `) |^ n = 0. X by Def1
.= a |^ (- n) by A1, Th3 ;
:: thesis: verum

end;

suppose A2: n > 0 ; :: thesis: (a `) |^ n = a |^ (- n)

set m = - n;
- (- n) > 0 by A2;
then A3: - n < 0 ;
then a |^ (- n) = (BCI-power X) . ((a `),|.(- n).|) by Def2
.= (BCI-power X) . ((a `),(- (- n))) by A3, ABSVALUE:def 1 ;
hence (a `) |^ n = a |^ (- n) ; :: thesis: verum

end;

end;