let G be Group; :: thesis:
let a be Element of G; :: thesis:
let A be Subset of G; :: thesis:
thus ( a in gr A implies ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) ) :: thesis:

proof

assume A1: a in gr A ; :: thesis:
defpred S₁[ set ] means ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( $1 = Product (F |^ I) & len F = len I & rng F c= A );
reconsider B = { b where b is Element of G : S₁[b] } as Subset of G from DOMAIN_1:sch 7();
( 1_ G = Product (<*> the carrier of G) & <*> the carrier of G = {} & (<*> the carrier of G) |^ (<*> INT ) = {} & rng (<*> the carrier of G) = {} & {} c= A & len {} = 0 & len (<*> INT ) = 0 ) by Th11, Th27, XBOOLE_1:2;
then A2: 1_ G in B ;

A3: now

let c, d be Element of G; :: thesis:
assume that
A4: c in B and
A5: d in B ; :: thesis:
A6: ex d1 being Element of G st
( c = d1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( d1 = Product (F |^ I) & len F = len I & rng F c= A ) ) by A4;
A7: ex d2 being Element of G st
( d = d2 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( d2 = Product (F |^ I) & len F = len I & rng F c= A ) ) by A5;
consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT such that
A8: c = Product (F1 |^ I1) and
A9: len F1 = len I1 and
A10: rng F1 c= A by A6;
consider F2 being FinSequence of the carrier of G, I2 being FinSequence of INT such that
A11: d = Product (F2 |^ I2) and
A12: len F2 = len I2 and
A13: rng F2 c= A by A7;
A14: c * d = Product ((F1 |^ I1) ^ (F2 |^ I2)) by A8, A11, Th8
.= Product ((F1 ^ F2) |^ (I1 ^ I2)) by A9, A12, Th25 ;
rng (F1 ^ F2) = (rng F1) \/ (rng F2) by FINSEQ_1:44;
then A15: rng (F1 ^ F2) c= A by A10, A13, XBOOLE_1:8;
len (F1 ^ F2) = (len I1) + (len I2) by A9, A12, FINSEQ_1:35
.= len (I1 ^ I2) by FINSEQ_1:35 ;
hence c * d in B by A14, A15; :: thesis:

end;

now

let c be Element of G; :: thesis:
assume c in B ; :: thesis:
then ex d1 being Element of G st
( c = d1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( d1 = Product (F |^ I) & len F = len I & rng F c= A ) ) ;
then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT such that
A16: c = Product (F1 |^ I1) and
A17: len F1 = len I1 and
A18: rng F1 c= A ;
A19: dom F1 = dom I1 by A17, FINSEQ_3:31;
deffunc H₁( Nat) -> set = F1 . (((len F1) - $1) + 1);
consider F2 being FinSequence such that
A20: len F2 = len F1 and
A21: for k being Nat st k in dom F2 holds
F2 . k = H₁(k) from FINSEQ_1:sch 2();
A22: Seg (len F1) = dom F1 by FINSEQ_1:def 3;
defpred S₂[ Nat, set ] means ex i being Integer st
( i = I1 . (((len I1) - $1) + 1) & $2 = - i );
A23: for k being Nat st k in Seg (len I1) holds
ex x being set st S₂[k,x]

proof

let k be Nat; :: thesis:
assume k in Seg (len I1) ; :: thesis:
then A24: k in dom I1 by FINSEQ_1:def 3;
then reconsider n = ((len I1) - k) + 1 as Element of NAT by Lm3;
( 1 <= n & n <= len I1 ) by A24, Lm3;
then n in dom I1 by FINSEQ_3:27;
then ( I1 . n in rng I1 & rng I1 c= INT ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider i = I1 . n as Element of INT ;
reconsider i = i as Integer ;
reconsider x = - i as set ;
take x ; :: thesis:
take i ; :: thesis:
thus ( i = I1 . (((len I1) - k) + 1) & x = - i ) ; :: thesis:

end;

consider I2 being FinSequence such that
A25: dom I2 = Seg (len I1) and
A26: for k being Nat st k in Seg (len I1) holds
S₂[k,I2 . k] from FINSEQ_1:sch 1(A23);
A27: Seg (len I1) = dom I1 by FINSEQ_1:def 3;
A28: len F2 = len I2 by A17, A20, A25, FINSEQ_1:def 3;
A29: dom F2 = dom I2 by A17, A20, A25, FINSEQ_1:def 3;
A30: rng F2 c= rng F1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng F2 ; :: thesis:
then consider y being set such that
A31: ( y in dom F2 & F2 . y = x ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A31;
A32: x = F1 . (((len F1) - y) + 1) by A21, A31;
reconsider n = ((len F1) - y) + 1 as Element of NAT by A20, A31, Lm3;
A33: 1 <= n by A20, A31, Lm3;
n <= len F1 by A20, A31, Lm3;
then n in dom F1 by A33, FINSEQ_3:27;
hence x in rng F1 by A32, FUNCT_1:def 5; :: thesis:

end;

then A34: rng F2 c= A by A18, XBOOLE_1:1;
rng F1 c= the carrier of G by FINSEQ_1:def 4;
then rng F2 c= the carrier of G by A30, XBOOLE_1:1;
then reconsider F2 = F2 as FinSequence of the carrier of G by FINSEQ_1:def 4;
rng I2 c= INT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng I2 ; :: thesis:
then consider y being set such that
A35: y in dom I2 and
A36: x = I2 . y by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A35;
ex i being Integer st
( i = I1 . (((len I1) - y) + 1) & x = - i ) by A25, A26, A35, A36;
hence x in INT by INT_1:def 2; :: thesis:

end;

now

let k be Element of NAT ; :: thesis:
assume A39: k in dom (F2 |^ I2) ; :: thesis:
then reconsider n = ((len (F1 |^ I1)) - k) + 1 as Element of NAT by A20, A37, Lm3;
( 1 <= n & len (F1 |^ I1) >= n ) by A20, A37, A39, Lm3;
then A40: ( n in dom I2 & n in Seg (len I2) ) by A20, A28, A37, FINSEQ_1:3, FINSEQ_3:27;
dom (F2 |^ I2) = dom I1 by A17, A20, A37, FINSEQ_3:31;
then consider i being Integer such that
A41: ( i = I1 . n & I2 . k = - i ) by A17, A26, A27, A37, A39;
( I2 . k = I2 /. k & I2 /. k = @ (I2 /. k) ) by A29, A38, A39, PARTFUN1:def 8;
then ( (F2 |^ I2) . k = (F2 /. k) |^ (- i) & F2 /. k = F2 . k & F2 . k = F1 . n & F1 /. n = F1 . n ) by A17, A21, A22, A25, A37, A38, A39, A40, A41, Def4, PARTFUN1:def 8;
then A42: (F2 |^ I2) . k = ((F1 /. n) |^ i) " by GROUP_1:70;
( I1 . n = I1 /. n & I1 /. n = @ (I1 /. n) ) by A25, A27, A40, PARTFUN1:def 8;
then (F1 |^ I1) . n = (F1 /. n) |^ i by A19, A25, A27, A40, A41, Def4;
then ( ((F1 |^ I1) /. n) " = ((F1 /. n) |^ i) " & (F2 |^ I2) /. k = (F2 |^ I2) . k ) by A19, A25, A27, A38, A39, A40, PARTFUN1:def 8;
then (F1 |^ I1) /. n = ((F2 |^ I2) /. k) " by A42;
hence ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1) by A19, A25, A27, A38, A40, PARTFUN1:def 8; :: thesis:

end;

then (Product (F1 |^ I1)) " = Product (F2 |^ I2) by A20, A37, Th17;
hence c " in B by A16, A28, A34; :: thesis:

end;

then consider H being strict Subgroup of G such that
A43: the carrier of H = B by A2, A3, GROUP_2:61;
A c= B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A44: x in A ; :: thesis:
then reconsider a = x as Element of G ;
reconsider p = 1 as Integer ;
A45: ( len <*a*> = 1 & len <*(@ p)*> = 1 ) by FINSEQ_1:56;
A46: Product (<*a*> |^ <*(@ p)*>) = Product <*(a |^ 1)*> by Th28
.= a |^ 1 by FINSOP_1:12
.= a by GROUP_1:44 ;
( rng <*a*> = {a} & {a} c= A ) by A44, FINSEQ_1:56, ZFMISC_1:37;
hence x in B by A45, A46; :: thesis:

end;

then gr A is Subgroup of H by A43, Def5;
then a in H by A1, GROUP_2:49;
then a in B by A43, STRUCT_0:def 5;
then ex b being Element of G st
( b = a & ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( b = Product (F |^ I) & len F = len I & rng F c= A ) ) ;
hence ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= A & Product (F |^ I) = a ) ; :: thesis:

end;

given F being FinSequence of the carrier of G, I being FinSequence of INT such that len F = len I and
A47: rng F c= A and
A48: Product (F |^ I) = a ; :: thesis:
A c= the carrier of (gr A) by Def5;
then rng F c= carr (gr A) by A47, XBOOLE_1:1;
hence a in gr A by A48, Th26; :: thesis: