let O be set ; :: thesis: for G being GroupWithOperators of O

for A being Subset of G

for g1 being Element of G holds

( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )

let G be GroupWithOperators of O; :: thesis: for A being Subset of G

for g1 being Element of G holds

( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )

let A be Subset of G; :: thesis: for g1 being Element of G holds

( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )

let g1 be Element of G; :: thesis: ( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )

set H9 = the_stable_subgroup_of A;

set Y = the carrier of (the_stable_subgroup_of A);

A1: A c= the carrier of (the_stable_subgroup_of A) by Def26;

thus ( g1 in the_stable_subgroup_of A implies ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) ) :: thesis: ( ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) implies g1 in the_stable_subgroup_of A )

len F = len I and

A77: rng F c= C and

A78: Product (F |^ I) = g1 ; :: thesis: g1 in the_stable_subgroup_of A

the_stable_subgroup_of A is Subgroup of G by Def7;

then reconsider Y = the carrier of (the_stable_subgroup_of A) as Subset of G by GROUP_2:def 5;

reconsider H9 = the_stable_subgroup_of A as Subgroup of G by Def7;

C c= the carrier of H9 by A76, A1, A84, Def2;

then rng F c= carr H9 by A77;

hence g1 in the_stable_subgroup_of A by A78, GROUP_4:20; :: thesis: verum

for A being Subset of G

for g1 being Element of G holds

( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )

let G be GroupWithOperators of O; :: thesis: for A being Subset of G

for g1 being Element of G holds

( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )

let A be Subset of G; :: thesis: for g1 being Element of G holds

( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )

let g1 be Element of G; :: thesis: ( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )

set H9 = the_stable_subgroup_of A;

set Y = the carrier of (the_stable_subgroup_of A);

A1: A c= the carrier of (the_stable_subgroup_of A) by Def26;

thus ( g1 in the_stable_subgroup_of A implies ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) ) :: thesis: ( ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) implies g1 in the_stable_subgroup_of A )

proof

given F being FinSequence of the carrier of G, I being FinSequence of INT , C being Subset of G such that A76:
C = the_stable_subset_generated_by (A, the action of G)
and
defpred S_{1}[ set ] means ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & $1 = Product (F |^ I) & len F = len I & rng F c= C );

assume A2: g1 in the_stable_subgroup_of A ; :: thesis: ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 )

reconsider B = { b where b is Element of G : S_{1}[b] } as Subset of G from DOMAIN_1:sch 7();

( 1_ G = Product (<*> the carrier of G) & (<*> the carrier of G) |^ (<*> INT) = {} ) by GROUP_4:8, GROUP_4:21;

then 1_ G in B by A71;

then consider H being strict StableSubgroup of G such that

A72: the carrier of H = B by A3, A35, A16, Lm14;

A c= B

then the_stable_subgroup_of A is Subgroup of H by Def7;

then g1 in H by A2, GROUP_2:40;

then g1 in B by A72, STRUCT_0:def 5;

then ex b being Element of G st

( b = g1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & b = Product (F |^ I) & len F = len I & rng F c= C ) ) ;

hence ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) ; :: thesis: verum

end;( C = the_stable_subset_generated_by (A, the action of G) & $1 = Product (F |^ I) & len F = len I & rng F c= C );

assume A2: g1 in the_stable_subgroup_of A ; :: thesis: ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 )

reconsider B = { b where b is Element of G : S

A3: now :: thesis: for c, d being Element of G st c in B & d in B holds

c * d in B

c * d in B

let c, d be Element of G; :: thesis: ( c in B & d in B implies c * d in B )

assume that

A4: c in B and

A5: d in B ; :: thesis: c * d in B

ex d1 being Element of G st

( c = d1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & d1 = Product (F |^ I) & len F = len I & rng F c= C ) ) by A4;

then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT , C being Subset of G such that

A6: C = the_stable_subset_generated_by (A, the action of G) and

A7: c = Product (F1 |^ I1) and

A8: len F1 = len I1 and

A9: rng F1 c= C ;

ex d2 being Element of G st

( d = d2 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & d2 = Product (F |^ I) & len F = len I & rng F c= C ) ) by A5;

then consider F2 being FinSequence of the carrier of G, I2 being FinSequence of INT , C being Subset of G such that

A10: C = the_stable_subset_generated_by (A, the action of G) and

A11: d = Product (F2 |^ I2) and

A12: len F2 = len I2 and

A13: rng F2 c= C ;

A14: len (F1 ^ F2) = (len I1) + (len I2) by A8, A12, FINSEQ_1:22

.= len (I1 ^ I2) by FINSEQ_1:22 ;

rng (F1 ^ F2) = (rng F1) \/ (rng F2) by FINSEQ_1:31;

then A15: rng (F1 ^ F2) c= C by A6, A9, A10, A13, XBOOLE_1:8;

c * d = Product ((F1 |^ I1) ^ (F2 |^ I2)) by A7, A11, GROUP_4:5

.= Product ((F1 ^ F2) |^ (I1 ^ I2)) by A8, A12, GROUP_4:19 ;

hence c * d in B by A10, A15, A14; :: thesis: verum

end;assume that

A4: c in B and

A5: d in B ; :: thesis: c * d in B

ex d1 being Element of G st

( c = d1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & d1 = Product (F |^ I) & len F = len I & rng F c= C ) ) by A4;

then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT , C being Subset of G such that

A6: C = the_stable_subset_generated_by (A, the action of G) and

A7: c = Product (F1 |^ I1) and

A8: len F1 = len I1 and

A9: rng F1 c= C ;

ex d2 being Element of G st

( d = d2 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & d2 = Product (F |^ I) & len F = len I & rng F c= C ) ) by A5;

then consider F2 being FinSequence of the carrier of G, I2 being FinSequence of INT , C being Subset of G such that

A10: C = the_stable_subset_generated_by (A, the action of G) and

A11: d = Product (F2 |^ I2) and

A12: len F2 = len I2 and

A13: rng F2 c= C ;

A14: len (F1 ^ F2) = (len I1) + (len I2) by A8, A12, FINSEQ_1:22

.= len (I1 ^ I2) by FINSEQ_1:22 ;

rng (F1 ^ F2) = (rng F1) \/ (rng F2) by FINSEQ_1:31;

then A15: rng (F1 ^ F2) c= C by A6, A9, A10, A13, XBOOLE_1:8;

c * d = Product ((F1 |^ I1) ^ (F2 |^ I2)) by A7, A11, GROUP_4:5

.= Product ((F1 ^ F2) |^ (I1 ^ I2)) by A8, A12, GROUP_4:19 ;

hence c * d in B by A10, A15, A14; :: thesis: verum

A16: now :: thesis: for o being Element of O

for c being Element of G st c in B holds

(G ^ o) . c in B

for c being Element of G st c in B holds

(G ^ o) . c in B

let o be Element of O; :: thesis: for c being Element of G st c in B holds

(G ^ o) . c in B

let c be Element of G; :: thesis: ( c in B implies (G ^ o) . c in B )

assume c in B ; :: thesis: (G ^ o) . c in B

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 ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & d1 = Product (F |^ I) & len F = len I & rng F c= C ) ) ;

then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT , C being Subset of G such that

A17: C = the_stable_subset_generated_by (A, the action of G) and

A18: c = Product (F1 |^ I1) and

A19: len F1 = len I1 and

A20: rng F1 c= C ;

deffunc H_{1}( Nat) -> set = (G ^ o) . (F1 . $1);

consider F2 being FinSequence such that

A21: len F2 = len F1 and

A22: for k being Nat st k in dom F2 holds

F2 . k = H_{1}(k)
from FINSEQ_1:sch 2();

A23: dom F2 = dom F1 by A21, FINSEQ_3:29;

A24: Seg (len F1) = dom F1 by FINSEQ_1:def 3;

then rng F2 c= the carrier of G by XBOOLE_1:1;

then reconsider F2 = F2 as FinSequence of the carrier of G by FINSEQ_1:def 4;

(G ^ o) . c = Product (F2 |^ I1) by A18, A19, A21, A22, A23, Lm23;

hence (G ^ o) . c in B by A17, A19, A21, A34; :: thesis: verum

end;(G ^ o) . c in B

let c be Element of G; :: thesis: ( c in B implies (G ^ o) . c in B )

assume c in B ; :: thesis: (G ^ o) . c in B

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 ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & d1 = Product (F |^ I) & len F = len I & rng F c= C ) ) ;

then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT , C being Subset of G such that

A17: C = the_stable_subset_generated_by (A, the action of G) and

A18: c = Product (F1 |^ I1) and

A19: len F1 = len I1 and

A20: rng F1 c= C ;

deffunc H

consider F2 being FinSequence such that

A21: len F2 = len F1 and

A22: for k being Nat st k in dom F2 holds

F2 . k = H

A23: dom F2 = dom F1 by A21, FINSEQ_3:29;

A24: Seg (len F1) = dom F1 by FINSEQ_1:def 3;

now :: thesis: for y being object st y in rng F2 holds

y in C

then A34:
rng F2 c= C
;y in C

A25:
C is_stable_under_the_action_of the action of G
by A17, Def2;

let y be object ; :: thesis: ( y in rng F2 implies b_{1} in C )

assume y in rng F2 ; :: thesis: b_{1} in C

then consider x being object such that

A26: x in dom F2 and

A27: y = F2 . x by FUNCT_1:def 3;

A28: x in Seg (len F1) by A21, A26, FINSEQ_1:def 3;

reconsider x = x as Element of NAT by A26;

A29: F2 . x = (G ^ o) . (F1 . x) by A22, A26;

A30: F1 . x in rng F1 by A24, A28, FUNCT_1:3;

end;let y be object ; :: thesis: ( y in rng F2 implies b

assume y in rng F2 ; :: thesis: b

then consider x being object such that

A26: x in dom F2 and

A27: y = F2 . x by FUNCT_1:def 3;

A28: x in Seg (len F1) by A21, A26, FINSEQ_1:def 3;

reconsider x = x as Element of NAT by A26;

A29: F2 . x = (G ^ o) . (F1 . x) by A22, A26;

A30: F1 . x in rng F1 by A24, A28, FUNCT_1:3;

per cases
( O <> {} or O = {} )
;

end;

suppose A31:
O <> {}
; :: thesis: b_{1} in C

set f = the action of G . o;

A32: G ^ o = the action of G . o by A31, Def6;

then reconsider f = the action of G . o as Function of G,G ;

dom f = the carrier of G by FUNCT_2:def 1;

then A33: y in f .: C by A20, A27, A29, A30, A32, FUNCT_1:def 6;

f .: C c= C by A25, A31;

hence y in C by A33; :: thesis: verum

end;A32: G ^ o = the action of G . o by A31, Def6;

then reconsider f = the action of G . o as Function of G,G ;

dom f = the carrier of G by FUNCT_2:def 1;

then A33: y in f .: C by A20, A27, A29, A30, A32, FUNCT_1:def 6;

f .: C c= C by A25, A31;

hence y in C by A33; :: thesis: verum

then rng F2 c= the carrier of G by XBOOLE_1:1;

then reconsider F2 = F2 as FinSequence of the carrier of G by FINSEQ_1:def 4;

(G ^ o) . c = Product (F2 |^ I1) by A18, A19, A21, A22, A23, Lm23;

hence (G ^ o) . c in B by A17, A19, A21, A34; :: thesis: verum

A35: now :: thesis: for c being Element of G st c in B holds

c " in B

A71:
( rng (<*> the carrier of G) = {} & {} c= the_stable_subset_generated_by (A, the action of G) )
;c " in B

let c be Element of G; :: thesis: ( c in B implies c " in B )

assume c in B ; :: thesis: c " in B

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 ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & d1 = Product (F |^ I) & len F = len I & rng F c= C ) ) ;

then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT , C being Subset of G such that

A36: ( C = the_stable_subset_generated_by (A, the action of G) & c = Product (F1 |^ I1) ) and

A37: len F1 = len I1 and

A38: rng F1 c= C ;

deffunc H_{1}( Nat) -> set = F1 . (((len F1) - $1) + 1);

consider F2 being FinSequence such that

A39: len F2 = len F1 and

A40: for k being Nat st k in dom F2 holds

F2 . k = H_{1}(k)
from FINSEQ_1:sch 2();

A41: Seg (len I1) = dom I1 by FINSEQ_1:def 3;

A42: rng F2 c= rng F1

set p = F1 |^ I1;

A47: Seg (len F1) = dom F1 by FINSEQ_1:def 3;

A48: len (F1 |^ I1) = len F1 by GROUP_4:def 3;

defpred S_{2}[ Nat, object ] means ex i being Integer st

( i = I1 . (((len I1) - $1) + 1) & $2 = - i );

A49: for k being Nat st k in Seg (len I1) holds

ex x being object st S_{2}[k,x]

A51: dom I2 = Seg (len I1) and

A52: for k being Nat st k in Seg (len I1) holds

S_{2}[k,I2 . k]
from FINSEQ_1:sch 1(A49);

A53: len F2 = len I2 by A37, A39, A51, FINSEQ_1:def 3;

A54: rng I2 c= INT

A58: dom F2 = dom I2 by A37, A39, A51, FINSEQ_1:def 3;

reconsider I2 = I2 as FinSequence of INT by A54, FINSEQ_1:def 4;

reconsider F2 = F2 as FinSequence of the carrier of G by A57, FINSEQ_1:def 4;

set q = F2 |^ I2;

A59: len (F2 |^ I2) = len F2 by GROUP_4:def 3;

then A60: dom (F2 |^ I2) = dom F2 by FINSEQ_3:29;

A61: dom F1 = dom I1 by A37, FINSEQ_3:29;

hence c " in B by A36, A53, A46; :: thesis: verum

end;assume c in B ; :: thesis: c " in B

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 ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & d1 = Product (F |^ I) & len F = len I & rng F c= C ) ) ;

then consider F1 being FinSequence of the carrier of G, I1 being FinSequence of INT , C being Subset of G such that

A36: ( C = the_stable_subset_generated_by (A, the action of G) & c = Product (F1 |^ I1) ) and

A37: len F1 = len I1 and

A38: rng F1 c= C ;

deffunc H

consider F2 being FinSequence such that

A39: len F2 = len F1 and

A40: for k being Nat st k in dom F2 holds

F2 . k = H

A41: Seg (len I1) = dom I1 by FINSEQ_1:def 3;

A42: rng F2 c= rng F1

proof

then A46:
rng F2 c= C
by A38;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F2 or x in rng F1 )

assume x in rng F2 ; :: thesis: x in rng F1

then consider y being object such that

A43: y in dom F2 and

A44: F2 . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A43;

reconsider n = ((len F1) - y) + 1 as Element of NAT by A39, A43, Lm22;

( 1 <= n & n <= len F1 ) by A39, A43, Lm22;

then A45: n in dom F1 by FINSEQ_3:25;

x = F1 . (((len F1) - y) + 1) by A40, A43, A44;

hence x in rng F1 by A45, FUNCT_1:def 3; :: thesis: verum

end;assume x in rng F2 ; :: thesis: x in rng F1

then consider y being object such that

A43: y in dom F2 and

A44: F2 . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A43;

reconsider n = ((len F1) - y) + 1 as Element of NAT by A39, A43, Lm22;

( 1 <= n & n <= len F1 ) by A39, A43, Lm22;

then A45: n in dom F1 by FINSEQ_3:25;

x = F1 . (((len F1) - y) + 1) by A40, A43, A44;

hence x in rng F1 by A45, FUNCT_1:def 3; :: thesis: verum

set p = F1 |^ I1;

A47: Seg (len F1) = dom F1 by FINSEQ_1:def 3;

A48: len (F1 |^ I1) = len F1 by GROUP_4:def 3;

defpred S

( i = I1 . (((len I1) - $1) + 1) & $2 = - i );

A49: for k being Nat st k in Seg (len I1) holds

ex x being object st S

proof

consider I2 being FinSequence such that
let k be Nat; :: thesis: ( k in Seg (len I1) implies ex x being object st S_{2}[k,x] )

assume k in Seg (len I1) ; :: thesis: ex x being object st S_{2}[k,x]

then A50: k in dom I1 by FINSEQ_1:def 3;

then reconsider n = ((len I1) - k) + 1 as Element of NAT by Lm22;

( 1 <= n & n <= len I1 ) by A50, Lm22;

then n in dom I1 by FINSEQ_3:25;

then I1 . n in rng I1 by FUNCT_1:def 3;

then reconsider i = I1 . n as Element of INT ;

take - i ; :: thesis: S_{2}[k, - i]

take i ; :: thesis: ( i = I1 . (((len I1) - k) + 1) & - i = - i )

thus ( i = I1 . (((len I1) - k) + 1) & - i = - i ) ; :: thesis: verum

end;assume k in Seg (len I1) ; :: thesis: ex x being object st S

then A50: k in dom I1 by FINSEQ_1:def 3;

then reconsider n = ((len I1) - k) + 1 as Element of NAT by Lm22;

( 1 <= n & n <= len I1 ) by A50, Lm22;

then n in dom I1 by FINSEQ_3:25;

then I1 . n in rng I1 by FUNCT_1:def 3;

then reconsider i = I1 . n as Element of INT ;

take - i ; :: thesis: S

take i ; :: thesis: ( i = I1 . (((len I1) - k) + 1) & - i = - i )

thus ( i = I1 . (((len I1) - k) + 1) & - i = - i ) ; :: thesis: verum

A51: dom I2 = Seg (len I1) and

A52: for k being Nat st k in Seg (len I1) holds

S

A53: len F2 = len I2 by A37, A39, A51, FINSEQ_1:def 3;

A54: rng I2 c= INT

proof

A57:
rng F2 c= the carrier of G
by A42, XBOOLE_1:1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng I2 or x in INT )

assume x in rng I2 ; :: thesis: x in INT

then consider y being object such that

A55: y in dom I2 and

A56: x = I2 . y by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A55;

ex i being Integer st

( i = I1 . (((len I1) - y) + 1) & x = - i ) by A51, A52, A55, A56;

hence x in INT by INT_1:def 2; :: thesis: verum

end;assume x in rng I2 ; :: thesis: x in INT

then consider y being object such that

A55: y in dom I2 and

A56: x = I2 . y by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A55;

ex i being Integer st

( i = I1 . (((len I1) - y) + 1) & x = - i ) by A51, A52, A55, A56;

hence x in INT by INT_1:def 2; :: thesis: verum

A58: dom F2 = dom I2 by A37, A39, A51, FINSEQ_1:def 3;

reconsider I2 = I2 as FinSequence of INT by A54, FINSEQ_1:def 4;

reconsider F2 = F2 as FinSequence of the carrier of G by A57, FINSEQ_1:def 4;

set q = F2 |^ I2;

A59: len (F2 |^ I2) = len F2 by GROUP_4:def 3;

then A60: dom (F2 |^ I2) = dom F2 by FINSEQ_3:29;

A61: dom F1 = dom I1 by A37, FINSEQ_3:29;

now :: thesis: for k being Nat st k in dom (F2 |^ I2) holds

((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1)

then
(Product (F1 |^ I1)) " = Product (F2 |^ I2)
by A39, A48, A59, GROUP_4:14;((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1)

let k be Nat; :: thesis: ( k in dom (F2 |^ I2) implies ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1) )

A62: I2 /. k = @ (I2 /. k) ;

assume A63: k in dom (F2 |^ I2) ; :: thesis: ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1)

then reconsider n = ((len (F1 |^ I1)) - k) + 1 as Element of NAT by A39, A48, A59, Lm22;

A64: ( I1 /. n = @ (I1 /. n) & (F2 |^ I2) /. k = (F2 |^ I2) . k ) by A63, PARTFUN1:def 6;

A65: ( F2 /. k = F2 . k & F2 . k = F1 . n ) by A40, A48, A60, A63, PARTFUN1:def 6;

( 1 <= n & len (F1 |^ I1) >= n ) by A39, A48, A59, A63, Lm22;

then A66: n in dom I2 by A37, A51, A48;

then A67: I1 . n = I1 /. n by A51, A41, PARTFUN1:def 6;

dom (F2 |^ I2) = dom I1 by A37, A39, A59, FINSEQ_3:29;

then consider i being Integer such that

A68: i = I1 . n and

A69: I2 . k = - i by A37, A52, A41, A48, A63;

I2 . k = I2 /. k by A58, A60, A63, PARTFUN1:def 6;

then A70: (F2 |^ I2) . k = (F2 /. k) |^ (- i) by A60, A63, A69, A62, GROUP_4:def 3;

F1 /. n = F1 . n by A37, A47, A51, A66, PARTFUN1:def 6;

then (F2 |^ I2) . k = ((F1 /. n) |^ i) " by A70, A65, GROUP_1:36;

hence ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1) by A61, A51, A41, A66, A68, A67, A64, GROUP_4:def 3; :: thesis: verum

end;A62: I2 /. k = @ (I2 /. k) ;

assume A63: k in dom (F2 |^ I2) ; :: thesis: ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1)

then reconsider n = ((len (F1 |^ I1)) - k) + 1 as Element of NAT by A39, A48, A59, Lm22;

A64: ( I1 /. n = @ (I1 /. n) & (F2 |^ I2) /. k = (F2 |^ I2) . k ) by A63, PARTFUN1:def 6;

A65: ( F2 /. k = F2 . k & F2 . k = F1 . n ) by A40, A48, A60, A63, PARTFUN1:def 6;

( 1 <= n & len (F1 |^ I1) >= n ) by A39, A48, A59, A63, Lm22;

then A66: n in dom I2 by A37, A51, A48;

then A67: I1 . n = I1 /. n by A51, A41, PARTFUN1:def 6;

dom (F2 |^ I2) = dom I1 by A37, A39, A59, FINSEQ_3:29;

then consider i being Integer such that

A68: i = I1 . n and

A69: I2 . k = - i by A37, A52, A41, A48, A63;

I2 . k = I2 /. k by A58, A60, A63, PARTFUN1:def 6;

then A70: (F2 |^ I2) . k = (F2 /. k) |^ (- i) by A60, A63, A69, A62, GROUP_4:def 3;

F1 /. n = F1 . n by A37, A47, A51, A66, PARTFUN1:def 6;

then (F2 |^ I2) . k = ((F1 /. n) |^ i) " by A70, A65, GROUP_1:36;

hence ((F2 |^ I2) /. k) " = (F1 |^ I1) . (((len (F1 |^ I1)) - k) + 1) by A61, A51, A41, A66, A68, A67, A64, GROUP_4:def 3; :: thesis: verum

hence c " in B by A36, A53, A46; :: thesis: verum

( 1_ G = Product (<*> the carrier of G) & (<*> the carrier of G) |^ (<*> INT) = {} ) by GROUP_4:8, GROUP_4:21;

then 1_ G in B by A71;

then consider H being strict StableSubgroup of G such that

A72: the carrier of H = B by A3, A35, A16, Lm14;

A c= B

proof

then
the_stable_subgroup_of A is StableSubgroup of H
by A72, Def26;
set C = the_stable_subset_generated_by (A, the action of G);

reconsider p = 1 as Integer ;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )

assume A73: x in A ; :: thesis: x in B

then reconsider a = x as Element of G ;

A c= the_stable_subset_generated_by (A, the action of G) by Def2;

then A74: ( rng <*a*> = {a} & {a} c= the_stable_subset_generated_by (A, the action of G) ) by A73, FINSEQ_1:39, ZFMISC_1:31;

A75: Product (<*a*> |^ <*(@ p)*>) = Product <*(a |^ 1)*> by GROUP_4:22

.= a |^ 1 by GROUP_4:9

.= a by GROUP_1:26 ;

( len <*a*> = 1 & len <*(@ p)*> = 1 ) by FINSEQ_1:39;

hence x in B by A75, A74; :: thesis: verum

end;reconsider p = 1 as Integer ;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )

assume A73: x in A ; :: thesis: x in B

then reconsider a = x as Element of G ;

A c= the_stable_subset_generated_by (A, the action of G) by Def2;

then A74: ( rng <*a*> = {a} & {a} c= the_stable_subset_generated_by (A, the action of G) ) by A73, FINSEQ_1:39, ZFMISC_1:31;

A75: Product (<*a*> |^ <*(@ p)*>) = Product <*(a |^ 1)*> by GROUP_4:22

.= a |^ 1 by GROUP_4:9

.= a by GROUP_1:26 ;

( len <*a*> = 1 & len <*(@ p)*> = 1 ) by FINSEQ_1:39;

hence x in B by A75, A74; :: thesis: verum

then the_stable_subgroup_of A is Subgroup of H by Def7;

then g1 in H by A2, GROUP_2:40;

then g1 in B by A72, STRUCT_0:def 5;

then ex b being Element of G st

( b = g1 & ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & b = Product (F |^ I) & len F = len I & rng F c= C ) ) ;

hence ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st

( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) ; :: thesis: verum

len F = len I and

A77: rng F c= C and

A78: Product (F |^ I) = g1 ; :: thesis: g1 in the_stable_subgroup_of A

the_stable_subgroup_of A is Subgroup of G by Def7;

then reconsider Y = the carrier of (the_stable_subgroup_of A) as Subset of G by GROUP_2:def 5;

now :: thesis: for o being Element of O

for f being Function of G,G st o in O & f = the action of G . o holds

f .: Y c= Y

then A84:
Y is_stable_under_the_action_of the action of G
;for f being Function of G,G st o in O & f = the action of G . o holds

f .: Y c= Y

let o be Element of O; :: thesis: for f being Function of G,G st o in O & f = the action of G . o holds

f .: Y c= Y

let f be Function of G,G; :: thesis: ( o in O & f = the action of G . o implies f .: Y c= Y )

assume A79: o in O ; :: thesis: ( f = the action of G . o implies f .: Y c= Y )

assume A80: f = the action of G . o ; :: thesis: f .: Y c= Y

end;f .: Y c= Y

let f be Function of G,G; :: thesis: ( o in O & f = the action of G . o implies f .: Y c= Y )

assume A79: o in O ; :: thesis: ( f = the action of G . o implies f .: Y c= Y )

assume A80: f = the action of G . o ; :: thesis: f .: Y c= Y

now :: thesis: for y being object st y in f .: Y holds

y in Y

hence
f .: Y c= Y
; :: thesis: verumy in Y

let y be object ; :: thesis: ( y in f .: Y implies y in Y )

assume y in f .: Y ; :: thesis: y in Y

then consider x being object such that

A81: x in dom f and

A82: x in Y and

A83: y = f . x by FUNCT_1:def 6;

reconsider x = x as Element of G by A81;

x in the_stable_subgroup_of A by A82, STRUCT_0:def 5;

then (G ^ o) . x in the_stable_subgroup_of A by Lm9;

then f . x in the_stable_subgroup_of A by A79, A80, Def6;

hence y in Y by A83, STRUCT_0:def 5; :: thesis: verum

end;assume y in f .: Y ; :: thesis: y in Y

then consider x being object such that

A81: x in dom f and

A82: x in Y and

A83: y = f . x by FUNCT_1:def 6;

reconsider x = x as Element of G by A81;

x in the_stable_subgroup_of A by A82, STRUCT_0:def 5;

then (G ^ o) . x in the_stable_subgroup_of A by Lm9;

then f . x in the_stable_subgroup_of A by A79, A80, Def6;

hence y in Y by A83, STRUCT_0:def 5; :: thesis: verum

reconsider H9 = the_stable_subgroup_of A as Subgroup of G by Def7;

C c= the carrier of H9 by A76, A1, A84, Def2;

then rng F c= carr H9 by A77;

hence g1 in the_stable_subgroup_of A by A78, GROUP_4:20; :: thesis: verum