let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for m, n being Nat holds a |^ (n + m) = (a |^ m) \ ((a |^ n) `)
let a be Element of AtomSet X; :: thesis: for m, n being Nat holds a |^ (n + m) = (a |^ m) \ ((a |^ n) `)
let m, n be Nat; :: thesis: a |^ (n + m) = (a |^ m) \ ((a |^ n) `)
reconsider p = a |^ n as Element of AtomSet X by Th13;
defpred S<sub>1</sub>[ Nat] means a |^ (n + $1) = (a |^ $1) \ ((a |^ n) `);

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

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
reconsider q = a |^ (m + 1) as Element of AtomSet X by Th13;
assume A2: S₁[m] ; :: thesis: S₁[m + 1]
a |^ (n + (m + 1)) = a |^ ((n + m) + 1)
.= a \ (((a |^ m) \ ((a |^ n) `)) `) by A2, Th2
.= a \ (((a |^ m) `) \ (((a |^ n) `) `)) by BCIALG_1:9
.= a \ (((a |^ m) `) \ p) by BCIALG_1:29
.= p \ (((a |^ m) `) \ a) by Th1
.= (a |^ n) \ ((a |^ (m + 1)) `) by Th14
.= q \ (p `) by Th1
.= (a |^ (m + 1)) \ ((a |^ n) `) ;
hence S₁[m + 1] ; :: thesis: verum

end;

(a |^ 0) \ ((a |^ n) `) = ((a |^ n) `) ` by Def1
.= p by BCIALG_1:29 ;
then A3: S<sub>1</sub>[ 0 ] ;
for m being Nat holds S<sub>1</sub>[m] from NAT_1:sch 2(A3, A1);
hence a |^ (n + m) = (a |^ m) \ ((a |^ n) `) ; :: thesis: verum