let G be Group; :: thesis: for a, b being Element of G
for i being Integer holds (a |^ i) |^ b = (a |^ b) |^ i
let a, b be Element of G; :: thesis: for i being Integer holds (a |^ i) |^ b = (a |^ b) |^ i
let i be Integer; :: thesis: (a |^ i) |^ b = (a |^ b) |^ i

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

suppose i >= 0 ; :: thesis: (a |^ i) |^ b = (a |^ b) |^ i

then i = |.i.| by ABSVALUE:def 1;
hence (a |^ i) |^ b = (a |^ b) |^ i by Lm4; :: thesis: verum

end;

suppose A1: i < 0 ; :: thesis: (a |^ i) |^ b = (a |^ b) |^ i

hence (a |^ i) |^ b = ((a |^ |.i.|) ") |^ b by GROUP_1:30
.= ((a |^ |.i.|) |^ b) " by Th26
.= ((a |^ b) |^ |.i.|) " by Lm4
.= (a |^ b) |^ i by A1, GROUP_1:30 ;
:: thesis: verum

end;

end;