let O be set ; :: thesis: for E being non empty set

for A being Action of O,E

for X being Subset of E

for a being Element of E st not X is empty holds

( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a )

let E be non empty set ; :: thesis: for A being Action of O,E

for X being Subset of E

for a being Element of E st not X is empty holds

( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a )

let A be Action of O,E; :: thesis: for X being Subset of E

for a being Element of E st not X is empty holds

( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a )

let X be Subset of E; :: thesis: for a being Element of E st not X is empty holds

( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a )

let a be Element of E; :: thesis: ( not X is empty implies ( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a ) )

defpred S_{1}[ set ] means ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = $1;

set B = { e where e is Element of E : S_{1}[e] } ;

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

assume A1: not X is empty ; :: thesis: ( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a )

then A22: B = the_stable_subset_generated_by (X,A) by A20, A2, Def2;

thus a in the_stable_subset_generated_by (X,A) by A22, A26; :: thesis: verum

for A being Action of O,E

for X being Subset of E

for a being Element of E st not X is empty holds

( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a )

let E be non empty set ; :: thesis: for A being Action of O,E

for X being Subset of E

for a being Element of E st not X is empty holds

( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a )

let A be Action of O,E; :: thesis: for X being Subset of E

for a being Element of E st not X is empty holds

( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a )

let X be Subset of E; :: thesis: for a being Element of E st not X is empty holds

( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a )

let a be Element of E; :: thesis: ( not X is empty implies ( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a ) )

defpred S

set B = { e where e is Element of E : S

reconsider B = { e where e is Element of E : S

assume A1: not X is empty ; :: thesis: ( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a )

A2: now :: thesis: for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds

B c= Y

B c= Y

let Y be Subset of E; :: thesis: ( Y is_stable_under_the_action_of A & X c= Y implies B c= Y )

assume A3: Y is_stable_under_the_action_of A ; :: thesis: ( X c= Y implies B c= Y )

assume A4: X c= Y ; :: thesis: B c= Y

end;assume A3: Y is_stable_under_the_action_of A ; :: thesis: ( X c= Y implies B c= Y )

assume A4: X c= Y ; :: thesis: B c= Y

now :: thesis: for x being object st x in B holds

x in Y

hence
B c= Y
; :: thesis: verumx in Y

let x be object ; :: thesis: ( x in B implies x in Y )

assume x in B ; :: thesis: x in Y

then consider e being Element of E such that

A5: x = e and

A6: ex F being FinSequence of O ex x9 being Element of X st (Product (F,A)) . x9 = e ;

consider F being FinSequence of O, x9 being Element of X such that

A7: (Product (F,A)) . x9 = e by A6;

A8: x9 in X by A1;

then x9 in E ;

then x9 in dom (Product (F,A)) by FUNCT_2:def 1;

then A9: (Product (F,A)) . x9 in (Product (F,A)) .: Y by A4, A8, FUNCT_1:def 6;

(Product (F,A)) .: Y c= Y by A3, Lm29;

hence x in Y by A5, A7, A9; :: thesis: verum

end;assume x in B ; :: thesis: x in Y

then consider e being Element of E such that

A5: x = e and

A6: ex F being FinSequence of O ex x9 being Element of X st (Product (F,A)) . x9 = e ;

consider F being FinSequence of O, x9 being Element of X such that

A7: (Product (F,A)) . x9 = e by A6;

A8: x9 in X by A1;

then x9 in E ;

then x9 in dom (Product (F,A)) by FUNCT_2:def 1;

then A9: (Product (F,A)) . x9 in (Product (F,A)) .: Y by A4, A8, FUNCT_1:def 6;

(Product (F,A)) .: Y c= Y by A3, Lm29;

hence x in Y by A5, A7, A9; :: thesis: verum

now :: thesis: for o being Element of O

for f being Function of E,E st o in O & f = A . o holds

f .: B c= B

then A20:
B is_stable_under_the_action_of A
;for f being Function of E,E st o in O & f = A . o holds

f .: B c= B

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

b_{3} .: B c= B

let f be Function of E,E; :: thesis: ( o in O & f = A . o implies b_{2} .: B c= B )

assume A10: o in O ; :: thesis: ( f = A . o implies b_{2} .: B c= B )

assume A11: f = A . o ; :: thesis: b_{2} .: B c= B

end;b

let f be Function of E,E; :: thesis: ( o in O & f = A . o implies b

assume A10: o in O ; :: thesis: ( f = A . o implies b

assume A11: f = A . o ; :: thesis: b

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

end;

suppose A12:
O <> {}
; :: thesis: b_{2} .: B c= B

end;

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

y in B

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

reconsider o = o as Element of O ;

reconsider F99 = <*o*> as FinSequence of O by A12, FINSEQ_1:74;

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

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

then consider x being object such that

A13: x in dom f and

A14: x in B and

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

y in rng f by A13, A15, FUNCT_1:3;

then reconsider e = y as Element of E ;

consider e9 being Element of E such that

A16: e9 = x and

A17: ex F9 being FinSequence of O ex x9 being Element of X st (Product (F9,A)) . x9 = e9 by A14;

consider F9 being FinSequence of O, x9 being Element of X such that

A18: (Product (F9,A)) . x9 = e9 by A17;

reconsider F = F99 ^ F9 as FinSequence of O ;

x9 in X by A1;

then x9 in E ;

then A19: x9 in dom (Product (F9,A)) by FUNCT_2:def 1;

(Product (F,A)) . x9 = ((Product (F99,A)) * (Product (F9,A))) . x9 by A12, Lm28

.= (Product (F99,A)) . ((Product (F9,A)) . x9) by A19, FUNCT_1:13

.= e by A11, A12, A15, A16, A18, Lm25 ;

hence y in B ; :: thesis: verum

end;reconsider F99 = <*o*> as FinSequence of O by A12, FINSEQ_1:74;

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

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

then consider x being object such that

A13: x in dom f and

A14: x in B and

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

y in rng f by A13, A15, FUNCT_1:3;

then reconsider e = y as Element of E ;

consider e9 being Element of E such that

A16: e9 = x and

A17: ex F9 being FinSequence of O ex x9 being Element of X st (Product (F9,A)) . x9 = e9 by A14;

consider F9 being FinSequence of O, x9 being Element of X such that

A18: (Product (F9,A)) . x9 = e9 by A17;

reconsider F = F99 ^ F9 as FinSequence of O ;

x9 in X by A1;

then x9 in E ;

then A19: x9 in dom (Product (F9,A)) by FUNCT_2:def 1;

(Product (F,A)) . x9 = ((Product (F99,A)) * (Product (F9,A))) . x9 by A12, Lm28

.= (Product (F99,A)) . ((Product (F9,A)) . x9) by A19, FUNCT_1:13

.= e by A11, A12, A15, A16, A18, Lm25 ;

hence y in B ; :: thesis: verum

now :: thesis: for x being object st x in X holds

x in B

then
X c= B
;x in B

set F = <*> O;

let x be object ; :: thesis: ( x in X implies x in B )

assume A21: x in X ; :: thesis: x in B

then reconsider e = x as Element of E ;

reconsider x9 = e as Element of X by A21;

len (<*> O) = 0 ;

then (Product ((<*> O),A)) . x = (id E) . x by Def3

.= x by A21, FUNCT_1:18 ;

then (Product ((<*> O),A)) . x9 = e ;

hence x in B ; :: thesis: verum

end;let x be object ; :: thesis: ( x in X implies x in B )

assume A21: x in X ; :: thesis: x in B

then reconsider e = x as Element of E ;

reconsider x9 = e as Element of X by A21;

len (<*> O) = 0 ;

then (Product ((<*> O),A)) . x = (id E) . x by Def3

.= x by A21, FUNCT_1:18 ;

then (Product ((<*> O),A)) . x9 = e ;

hence x in B ; :: thesis: verum

then A22: B = the_stable_subset_generated_by (X,A) by A20, A2, Def2;

hereby :: thesis: ( ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a implies a in the_stable_subset_generated_by (X,A) )

given F being FinSequence of O, x being Element of X such that A26:
(Product (F,A)) . x = a
; :: thesis: a in the_stable_subset_generated_by (X,A)assume
a in the_stable_subset_generated_by (X,A)
; :: thesis: ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a

then consider e being Element of E such that

A23: a = e and

A24: ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = e by A22;

consider F being FinSequence of O, x being Element of X such that

A25: (Product (F,A)) . x = e by A24;

take F = F; :: thesis: ex x being Element of X st (Product (F,A)) . x = a

take x = x; :: thesis: (Product (F,A)) . x = a

thus (Product (F,A)) . x = a by A23, A25; :: thesis: verum

end;then consider e being Element of E such that

A23: a = e and

A24: ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = e by A22;

consider F being FinSequence of O, x being Element of X such that

A25: (Product (F,A)) . x = e by A24;

take F = F; :: thesis: ex x being Element of X st (Product (F,A)) . x = a

take x = x; :: thesis: (Product (F,A)) . x = a

thus (Product (F,A)) . x = a by A23, A25; :: thesis: verum

thus a in the_stable_subset_generated_by (X,A) by A22, A26; :: thesis: verum