let G be Group; :: thesis: for H being Subgroup of G
for a being Element of G st a in H holds
for j being Integer holds a |^ j in H
let H be Subgroup of G; :: thesis: for a being Element of G st a in H holds
for j being Integer holds a |^ j in H
let a be Element of G; :: thesis: ( a in H implies for j being Integer holds a |^ j in H )
assume A1: a in H ; :: thesis: for j being Integer holds a |^ j in H
let j be Integer; :: thesis: a |^ j in H
consider k being Element of NAT such that
A2: ( j = k or j = - k ) by INT_1:8;

per cases ( j = k or j = - k ) by A2;

suppose A3: j = k ; :: thesis: a |^ j in H

defpred S₁[ Element of NAT ] means a |^ $1 in H;
a |^ 0 = 1_ G by GROUP_1:43;
then A4: S₁[ 0 ] by GROUP_2:55;
A5: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then (a |^ n) * a in H by A1, GROUP_2:59;
hence S₁[n + 1] by GROUP_1:66; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A5);
hence a |^ j in H by A3; :: thesis: verum

end;

suppose A6: j = - k ; :: thesis: a |^ j in H

defpred S₁[ Element of NAT ] means a |^ (- $1) in H;
a |^ 0 = 1_ G by GROUP_1:43;
then A7: S₁[ 0 ] by GROUP_2:55;
A8: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A9: S₁[n] ; :: thesis: S₁[n + 1]
a " in H by A1, GROUP_2:60;
then (a |^ (- n)) * (a ") in H by A9, GROUP_2:59;
then (a |^ (- n)) * (a |^ (- 1)) in H by GROUP_1:62;
then a |^ ((- n) + (- 1)) in H by GROUP_1:63;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A7, A8);
hence a |^ j in H by A6; :: thesis: verum

end;

end;