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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: ( g * h = h * g implies g * (h |^ n) = (h |^ n) * g ) ; :: thesis: S₁[n + 1]
assume A3: g * h = h * g ; :: thesis: g * (h |^ (n + 1)) = (h |^ (n + 1)) * g
thus g * (h |^ (n + 1)) = g * (h * (h |^ n)) by Lm6
.= (g * h) * (h |^ n) by Def3
.= h * ((h |^ n) * g) by A2, A3, Def3
.= (h * (h |^ n)) * g by Def3
.= (h |^ (n + 1)) * g by Lm6 ; :: thesis: verum

end;

A4: S₁[ 0 ]

proof

assume g * h = h * g ; :: thesis: g * (h |^ 0) = (h |^ 0) * g
thus g * (h |^ 0) = g * (1_ G) by Def7
.= g by Def4
.= (1_ G) * g by Def4
.= (h |^ 0) * g by Def7 ; :: thesis: verum

end;

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