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 |^ (abs i) & h |^ j = h |^ (abs j) ) by Def9;
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 |^ (abs i)) * (h |^ (abs j)) = (h |^ (abs j)) * (g |^ (abs i)) by A1, Lm10;
( g |^ i = g |^ (abs i) & h |^ j = (h |^ (abs j)) " ) by A2, Def9;
hence (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i) by A3, Th28; :: thesis: verum

end;

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

A5: (g |^ (abs i)) * (h |^ (abs j)) = (h |^ (abs j)) * (g |^ (abs i)) by A1, Lm10;
( g |^ i = (g |^ (abs i)) " & h |^ j = h |^ (abs j) ) by A4, Def9;
hence (g |^ i) * (h |^ j) = (h |^ j) * (g |^ i) by A5, Th28; :: thesis: verum

end;

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

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

end;

end;