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 |^ (abs i) by Def9;
( (g * h) |^ i = (g * h) |^ (abs i) & g |^ i = g |^ (abs i) ) by A2, Def9;
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) |^ (abs i)) " by A1, Def9
.= ((h |^ (abs i)) * (g |^ (abs i))) " by A1, Lm11
.= ((g |^ (abs i)) " ) * ((h |^ (abs i)) " ) by Th25
.= (g |^ i) * ((h |^ (abs i)) " ) by A4, Def9
.= (g |^ i) * (h |^ i) by A4, Def9 ;
:: thesis: verum

end;

end;