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

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

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

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

end;

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

A3: (g |^ |.i.|) * (h |^ |.j.|) = (h |^ |.j.|) * (g |^ |.i.|) by A1, Lm10;
( g |^ i = g |^ |.i.| & h |^ j = (h |^ |.j.|) " ) by A2, Def8;
hence (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i) by A3, Th19; :: thesis: verum

end;

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

A5: (g |^ |.i.|) * (h |^ |.j.|) = (h |^ |.j.|) * (g |^ |.i.|) by A1, Lm10;
( g |^ i = (g |^ |.i.|) " & h |^ j = h |^ |.j.| ) by A4, Def8;
hence (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i) by A5, Th19; :: thesis: verum

end;

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

then A6: ( g |^ i = (g |^ |.i.|) " & h |^ j = (h |^ |.j.|) " ) by Def8;
hence (g |^ i) * (h |^ j) = ((h |^ |.j.|) * (g |^ |.i.|)) " by Th16
.= ((g |^ |.i.|) * (h |^ |.j.|)) " by A1, Lm10
.= (h |^ j) * (g |^ i) by A6, Th16 ;
:: thesis: verum

end;

end;