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

now

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

suppose i >= 0 ; :: thesis: a |^ i in H

then a |^ i = a |^ (abs i) by ABSVALUE:def 1;
hence a |^ i in H by A1, Th5; :: thesis: verum

end;

suppose i < 0 ; :: thesis: a |^ i in H

then ( a |^ i = (a |^ (abs i)) " & a |^ (abs i) in H ) by A1, Th5, GROUP_1:60;
hence a |^ i in H by GROUP_2:60; :: thesis: verum

end;

end;

end;

hence a |^ i in H ; :: thesis: verum