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

now :: thesis: a |^ i = h |^ i

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

suppose A2: i >= 0 ; :: thesis: a |^ i = h |^ i

hence a |^ i = a |^ |.i.| by ABSVALUE:def 1
.= h |^ |.i.| by A1, Th1
.= h |^ i by A2, ABSVALUE:def 1 ;
:: thesis: verum

end;

suppose A3: i < 0 ; :: thesis: a |^ i = h |^ i

A4: a |^ |.i.| = h |^ |.i.| by A1, Th1;
thus a |^ i = (a |^ |.i.|) " by A3, GROUP_1:30
.= (h |^ |.i.|) " by A4, GROUP_2:48
.= h |^ i by A3, GROUP_1:30 ; :: thesis: verum

end;

end;

end;

hence a |^ i = h |^ i ; :: thesis: verum