let R be non empty unital associative multMagma ; :: thesis: for a being Element of R
for n, m being Nat holds (a |^ n) |^ m = a |^ (n * m)
let a be Element of R; :: thesis: for n, m being Nat holds (a |^ n) |^ m = a |^ (n * m)
let n, m be Nat; :: thesis: (a |^ n) |^ m = a |^ (n * m)
defpred S₁[ Nat] means (power R) . ((a |^ n),$1) = (power R) . (a,(n * $1));

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] )
assume S₁[m] ; :: thesis: S₁[m + 1]
then (power R) . ((a |^ n),(m + 1)) = (a |^ (n * m)) * (a |^ n) by GROUP_1:def 7
.= a |^ ((n * m) + n) by Th10
.= (power R) . (a,(n * (m + 1))) ;
hence S₁[m + 1] ; :: thesis: verum

end;

(power R) . ((a |^ n),0) = 1_ R by GROUP_1:def 7
.= (power R) . (a,(n * 0)) by GROUP_1:def 7 ;
then A2: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A1);
hence (a |^ n) |^ m = a |^ (n * m) ; :: thesis: verum