let m, n be Nat; :: thesis: for G being Group
for h being Element of G holds h |^ (n * m) = (h |^ n) |^ m
let G be Group; :: thesis: for h being Element of G holds h |^ (n * m) = (h |^ n) |^ m
let h be Element of G; :: thesis: h |^ (n * m) = (h |^ n) |^ m
defpred S₁[ Nat] means for n being Nat holds h |^ (n * $1) = (h |^ n) |^ $1;
A1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: for n being Nat holds h |^ (n * m) = (h |^ n) |^ m ; :: thesis: S₁[m + 1]
let n be Nat; :: thesis: h |^ (n * (m + 1)) = (h |^ n) |^ (m + 1)
thus h |^ (n * (m + 1)) = h |^ ((n * m) + (n * 1))
.= (h |^ (n * m)) * (h |^ n) by Lm5
.= ((h |^ n) |^ m) * (h |^ n) by A2
.= ((h |^ n) |^ m) * ((h |^ n) |^ 1) by Th25
.= (h |^ n) |^ (m + 1) by Lm5 ; :: thesis: verum

end;

A3: S₁[ 0 ]

proof

let n be Nat; :: thesis: h |^ (n * 0) = (h |^ n) |^ 0
thus h |^ (n * 0) = 1_ G by Def7
.= (h |^ n) |^ 0 by Def7 ; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A3, A1);
hence h |^ (n * m) = (h |^ n) |^ m ; :: thesis: verum