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) `
set b = ((x `) `) |^ n;
(x `) ` in AtomSet X by BCIALG_1:34;
then reconsider b = ((x `) `) |^ n as Element of AtomSet X by Th13;
( 0. X in AtomSet X & x |^ n in BranchV b ) by Th20;
hence (x |^ n) ` = (((x `) `) |^ n) ` by BCIALG_1:37; :: thesis: verum