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

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

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

hence a |^ i = a |^ (abs i) by ABSVALUE:def 1
.= h |^ (abs i) by A1, Th3
.= h |^ i by A2, ABSVALUE:def 1 ;
:: thesis: verum

end;

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

A4: a |^ (abs i) = h |^ (abs i) by A1, Th3;
thus a |^ i = (a |^ (abs i)) " by A3, GROUP_1:60
.= (h |^ (abs i)) " by A4, GROUP_2:57
.= h |^ i by A3, GROUP_1:60 ; :: thesis: verum

end;

end;

end;

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