let G be Group; :: thesis: for b, a being Element of G holds
( b in gr {a} iff ex j1 being Integer st b = a |^ j1 )
let b, a be Element of G; :: thesis: ( b in gr {a} iff ex j1 being Integer st b = a |^ j1 )
A1: ( b in gr {a} implies ex j1 being Integer st b = a |^ j1 )

proof

assume b in gr {a} ; :: thesis: ex j1 being Integer st b = a |^ j1
then consider F being FinSequence of G, I being FinSequence of INT such that
A2: len F = len I and
A3: rng F c= {a} and
A4: Product (F |^ I) = b by GROUP_4:37;
take Sum I ; :: thesis: b = a |^ (Sum I)
A5: dom ((len F) |-> a) = Seg (len F) by FUNCOP_1:19
.= dom F by FINSEQ_1:def 3 ;
for p being Nat st p in dom F holds
F . p = ((len F) |-> a) . p

proof

let p be Nat; :: thesis: ( p in dom F implies F . p = ((len F) |-> a) . p )
A6: dom F = Seg (len F) by FINSEQ_1:def 3;
assume A7: p in dom F ; :: thesis: F . p = ((len F) |-> a) . p
then F . p in rng F by FUNCT_1:def 5;
then F . p = a by A3, TARSKI:def 1
.= ((len F) |-> a) . p by A6, A7, FUNCOP_1:13 ;
hence F . p = ((len F) |-> a) . p ; :: thesis: verum

end;

then b = Product (((len I) |-> a) |^ I) by A2, A4, A5, FINSEQ_1:17
.= a |^ (Sum I) by Th24 ;
hence b = a |^ (Sum I) ; :: thesis: verum

end;

( ex j1 being Integer st b = a |^ j1 implies b in gr {a} )

proof

given j1 being Integer such that A8: b = a |^ j1 ; :: thesis: b in gr {a}
consider n being Element of NAT such that
A9: ( j1 = n or j1 = - n ) by INT_1:8;

per cases ( j1 = n or j1 = - n ) by A9;

suppose A10: j1 = n ; :: thesis: b in gr {a}

ex F being FinSequence of G ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b )

proof

take F = n |-> a; :: thesis: ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b )
A11: len F = n by FINSEQ_1:def 18
.= len (n |-> (@ 1)) by FINSEQ_1:def 18 ;
A12: rng F c= {a} by FUNCOP_1:19;
Product (F |^ (n |-> (@ 1))) = Product (F |^ ((len F) |-> (@ 1))) by FINSEQ_1:def 18
.= Product (n |-> a) by GROUP_4:31
.= b by A8, A10, GROUP_4:15 ;
hence ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b ) by A11, A12; :: thesis: verum

end;

hence b in gr {a} by GROUP_4:37; :: thesis: verum

end;

suppose j1 = - n ; :: thesis: b in gr {a}

then A13: b " = a |^ (- (- n)) by A8, GROUP_1:70
.= a |^ n ;
ex F being FinSequence of G ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b " )

proof

take F = n |-> a; :: thesis: ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b " )
A14: len F = n by FINSEQ_1:def 18
.= len (n |-> (@ 1)) by FINSEQ_1:def 18 ;
A15: rng F c= {a} by FUNCOP_1:19;
Product (F |^ (n |-> (@ 1))) = Product (F |^ ((len F) |-> (@ 1))) by FINSEQ_1:def 18
.= Product (n |-> a) by GROUP_4:31
.= b " by A13, GROUP_4:15 ;
hence ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b " ) by A14, A15; :: thesis: verum

end;

then b " in gr {a} by GROUP_4:37;
then (b " ) " in gr {a} by GROUP_2:60;
hence b in gr {a} ; :: thesis: verum

end;

end;

end;

hence ( b in gr {a} iff ex j1 being Integer st b = a |^ j1 ) by A1; :: thesis: verum