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

proof

given j1 being Integer such that A2: b = a |^ j1 ; :: thesis: b in gr {a}
consider n being Nat such that
A3: ( j1 = n or j1 = - n ) by INT_1:2;

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

suppose A4: 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 )
A5: len F = n by CARD_1:def 7
.= len (n |-> (@ 1)) by CARD_1:def 7 ;
Product (F |^ (n |-> (@ 1))) = Product (F |^ ((len F) |-> (@ 1))) by CARD_1:def 7
.= Product (n |-> a) by GROUP_4:25
.= b by A2, A4, GROUP_4:12 ;
hence ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b ) by A5, FUNCOP_1:13; :: thesis: verum

end;

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

end;

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

then A6: b " = a |^ (- (- n)) by A2, GROUP_1:36
.= 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 " )
A7: len F = n by CARD_1:def 7
.= len (n |-> (@ 1)) by CARD_1:def 7 ;
Product (F |^ (n |-> (@ 1))) = Product (F |^ ((len F) |-> (@ 1))) by CARD_1:def 7
.= Product (n |-> a) by GROUP_4:25
.= b " by A6, GROUP_4:12 ;
hence ex I being FinSequence of INT st
( len F = len I & rng F c= {a} & Product (F |^ I) = b " ) by A7, FUNCOP_1:13; :: thesis: verum

end;

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

end;

end;

end;

( 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
A8: len F = len I and
A9: rng F c= {a} and
A10: Product (F |^ I) = b by GROUP_4:28;
take Sum I ; :: thesis: b = a |^ (Sum I)
A11: 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 )
A12: dom F = Seg (len F) by FINSEQ_1:def 3;
assume A13: p in dom F ; :: thesis: F . p = ((len F) |-> a) . p
then F . p in rng F by FUNCT_1:def 3;
then F . p = a by A9, TARSKI:def 1
.= ((len F) |-> a) . p by A12, A13, FUNCOP_1:7 ;
hence F . p = ((len F) |-> a) . p ; :: thesis: verum

end;

dom ((len F) |-> a) = Seg (len F) by FUNCOP_1:13
.= dom F by FINSEQ_1:def 3 ;
then b = Product (((len I) |-> a) |^ I) by A8, A10, A11, FINSEQ_1:13
.= a |^ (Sum I) by Th4 ;
hence b = a |^ (Sum I) ; :: thesis: verum

end;

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