let i be Integer; :: thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
(g * h) |^ i = (g |^ i) * (h |^ i)
let G be Group; :: thesis: for g, h being Element of G st g * h = h * g holds
(g * h) |^ i = (g |^ i) * (h |^ i)
let g, h be Element of G; :: thesis: ( g * h = h * g implies (g * h) |^ i = (g |^ i) * (h |^ i) )
assume A1: g * h = h * g ; :: thesis: (g * h) |^ i = (g |^ i) * (h |^ i)

per cases ( i >= 0 or i < 0 ) ;

suppose A2: i >= 0 ; :: thesis: (g * h) |^ i = (g |^ i) * (h |^ i)

then A3: h |^ i = h |^ |.i.| by Def8;
( (g * h) |^ i = (g * h) |^ |.i.| & g |^ i = g |^ |.i.| ) by A2, Def8;
hence (g * h) |^ i = (g |^ i) * (h |^ i) by A1, A3, Lm11; :: thesis: verum

end;

suppose A4: i < 0 ; :: thesis: (g * h) |^ i = (g |^ i) * (h |^ i)

hence (g * h) |^ i = ((h * g) |^ |.i.|) " by A1, Def8
.= ((h |^ |.i.|) * (g |^ |.i.|)) " by A1, Lm11
.= ((g |^ |.i.|) ") * ((h |^ |.i.|) ") by Th16
.= (g |^ i) * ((h |^ |.i.|) ") by A4, Def8
.= (g |^ i) * (h |^ i) by A4, Def8 ;
:: thesis: verum

end;

end;