let X be BCI-algebra; :: thesis: for a being Element of AtomSet X
for m, n being Nat holds (a |^ m) |^ n = a |^ (m * n)
let a be Element of AtomSet X; :: thesis: for m, n being Nat holds (a |^ m) |^ n = a |^ (m * n)
let m, n be Nat; :: thesis: (a |^ m) |^ n = a |^ (m * n)
defpred S₁[ Nat] means (a |^ m) |^ $1 = a |^ (m * $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]
then (a |^ m) |^ (n + 1) = (a |^ m) \ ((a |^ (m * n)) `) by Th2
.= a |^ (m + (m * n)) by Lm1
.= a |^ (m * (n + 1)) ;
hence S₁[n + 1] ; :: thesis: verum

end;

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