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 :: thesis: a |^ i in H

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

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

then a |^ i = a |^ |.i.| by ABSVALUE:def 1;
hence a |^ i in H by A1, Th3; :: thesis: verum

end;

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

then A2: a |^ i = (a |^ |.i.|) " by GROUP_1:30;
a |^ |.i.| in H by A1, Th3;
hence a |^ i in H by A2, GROUP_2:51; :: thesis: verum

end;

end;

end;

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