let n be Nat; :: thesis: for G being Group
for h being Element of G holds (h ") |^ n = (h |^ n) "
let G be Group; :: thesis: for h being Element of G holds (h ") |^ n = (h |^ n) "
let h be Element of G; :: thesis: (h ") |^ n = (h |^ n) "
defpred S₁[ Nat] means (h ") |^ $1 = (h |^ $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 (h ") |^ (n + 1) = ((h |^ n) ") * (h ") by Lm2
.= (h * (h |^ n)) " by Th16
.= (h |^ (n + 1)) " by Lm6 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(h ") |^ 0 = 1_ G by Def7
.= (1_ G) " by Th8
.= (h |^ 0) " by Def7 ;
then A2: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1);
hence (h ") |^ n = (h |^ n) " ; :: thesis: verum