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

end;

A4: S₁[ 0 ]

proof

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