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)) `
reconsider c = a ` as Element of AtomSet X by BCIALG_1:34;
c |^ (- n) = (c `) |^ n by Th10
.= (c |^ n) ` by Th17
.= (a |^ (- n)) ` by Th10 ;
hence (a `) |^ (- n) = (a |^ (- n)) ` ; :: thesis: verum