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 Th13;
(a |^ (n + 1)) ` = (a \ ((a |^ n) `)) ` by Th2
.= (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