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) `
defpred S₁[ Nat] means (a `) |^ $1 = (a |^ $1) ` ;

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
0. X in AtomSet X ;
then (a `) |^ (n + 1) = ((0. X) |^ (n + 1)) \ (a |^ (n + 1)) by Th15
.= (a |^ (n + 1)) ` by Th7 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(a `) |^ 0 = 0. X by Def1
.= (0. X) ` by BCIALG_1:def 5 ;
then A2: S₁[ 0 ] by Def1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1);
hence (a `) |^ n = (a |^ n) ` ; :: thesis: verum