let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for n being Nat holds (a |^ (n + 1)) ` = ((a |^ n) ` ) \ a
let a be Element of AtomSet X; :: thesis: for n being Nat holds (a |^ (n + 1)) ` = ((a |^ n) ` ) \ a
let n be Nat; :: thesis: (a |^ (n + 1)) ` = ((a |^ n) ` ) \ a
A1: a |^ n in AtomSet X by Th12;
(a |^ (n + 1)) ` = (a \ ((a |^ n) ` )) ` by Th1
.= (a ` ) \ (((a |^ n) ` ) ` ) by BCIALG_1:9
.= (a ` ) \ (a |^ n) by A1, BCIALG_1:29 ;
hence (a |^ (n + 1)) ` = ((a |^ n) ` ) \ a by BCIALG_1:7; :: thesis: verum