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 Th12;
B5: 0. X in AtomSet X ;
x |^ n in BranchV b by Th18;
hence (x |^ n) ` = (((x ` ) ` ) |^ n) ` by B5, BCIALG_1:37; :: thesis: verum