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 Nat such that

A2: ( j = k or j = - k ) by INT_1:2;

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 Nat such that

A2: ( j = k or j = - k ) by INT_1:2;

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

end;

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

defpred S_{1}[ Nat] means a |^ $1 in H;

a |^ 0 = 1_ G by GROUP_1:25;

then A4: S_{1}[ 0 ]
by GROUP_2:46;

A5: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A4, A5);

hence a |^ j in H by A3; :: thesis: verum

end;a |^ 0 = 1_ G by GROUP_1:25;

then A4: S

A5: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume S_{1}[n]
; :: thesis: S_{1}[n + 1]

then (a |^ n) * a in H by A1, GROUP_2:50;

hence S_{1}[n + 1]
by GROUP_1:34; :: thesis: verum

end;assume S

then (a |^ n) * a in H by A1, GROUP_2:50;

hence S

hence a |^ j in H by A3; :: thesis: verum

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

defpred S_{1}[ Nat] means a |^ (- $1) in H;

a |^ 0 = 1_ G by GROUP_1:25;

then A7: S_{1}[ 0 ]
by GROUP_2:46;

A8: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A7, A8);

hence a |^ j in H by A6; :: thesis: verum

end;a |^ 0 = 1_ G by GROUP_1:25;

then A7: S

A8: for n being Nat st S

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A9: S_{1}[n]
; :: thesis: S_{1}[n + 1]

a " in H by A1, GROUP_2:51;

then (a |^ (- n)) * (a ") in H by A9, GROUP_2:50;

then (a |^ (- n)) * (a |^ (- 1)) in H by GROUP_1:32;

then a |^ ((- n) + (- 1)) in H by GROUP_1:33;

hence S_{1}[n + 1]
; :: thesis: verum

end;assume A9: S

a " in H by A1, GROUP_2:51;

then (a |^ (- n)) * (a ") in H by A9, GROUP_2:50;

then (a |^ (- n)) * (a |^ (- 1)) in H by GROUP_1:32;

then a |^ ((- n) + (- 1)) in H by GROUP_1:33;

hence S

hence a |^ j in H by A6; :: thesis: verum