let m, n be Nat; :: thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n)
let G be Group; :: thesis: for g, h being Element of G st g * h = h * g holds
(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n)
let g, h be Element of G; :: thesis: ( g * h = h * g implies (g |^ n) * (h |^ m) = (h |^ m) * (g |^ n) )
defpred S₁[ Nat] means for m being Nat st g * h = h * g holds
(g |^ $1) * (h |^ m) = (h |^ m) * (g |^ $1);
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: for m being Nat st g * h = h * g holds
(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n) ; :: thesis: S₁[n + 1]
let m be Nat; :: thesis: ( g * h = h * g implies (g |^ (n + 1)) * (h |^ m) = (h |^ m) * (g |^ (n + 1)) )
assume A3: g * h = h * g ; :: thesis: (g |^ (n + 1)) * (h |^ m) = (h |^ m) * (g |^ (n + 1))
thus (g |^ (n + 1)) * (h |^ m) = (g * (g |^ n)) * (h |^ m) by Lm6
.= g * ((g |^ n) * (h |^ m)) by Def3
.= g * ((h |^ m) * (g |^ n)) by A2, A3
.= (g * (h |^ m)) * (g |^ n) by Def3
.= ((h |^ m) * g) * (g |^ n) by A3, Lm9
.= (h |^ m) * (g * (g |^ n)) by Def3
.= (h |^ m) * (g |^ (n + 1)) by Lm6 ; :: thesis: verum

end;

A4: S₁[ 0 ]

proof

let m be Nat; :: thesis: ( g * h = h * g implies (g |^ 0) * (h |^ m) = (h |^ m) * (g |^ 0) )
assume g * h = h * g ; :: thesis: (g |^ 0) * (h |^ m) = (h |^ m) * (g |^ 0)
thus (g |^ 0) * (h |^ m) = (1_ G) * (h |^ m) by Def7
.= h |^ m by Def4
.= (h |^ m) * (1_ G) by Def4
.= (h |^ m) * (g |^ 0) 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 |^ n) * (h |^ m) = (h |^ m) * (g |^ n) ) ; :: thesis: verum