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₁[ 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₁[e] } ;
reconsider B = { e where e is Element of E : S₁[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 )

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

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

now :: thesis: for x being object st x in B holds
x 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;

hence B c= Y ; :: thesis: verum

end;

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

let o be Element of O; :: thesis: for f being Function of E,E st o in O & f = A . o holds
b₃ .: B c= B
let f be Function of E,E; :: thesis: ( o in O & f = A . o implies b₂ .: B c= B )
assume A10: o in O ; :: thesis: ( f = A . o implies b₂ .: B c= B )
assume A11: f = A . o ; :: thesis: b₂ .: B c= B

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

suppose O = {} ; :: thesis: b₂ .: B c= B

hence f .: B c= B by A10; :: thesis: verum

end;

suppose A12: O <> {} ; :: thesis: b₂ .: B c= B

now :: thesis: for y being object st y in f .: B holds
y 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;

hence f .: B c= B ; :: thesis: verum

end;

end;

end;

then A20: B is_stable_under_the_action_of A ;

now :: thesis: for x being object st x in X holds
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;

then X c= B ;
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) )

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;

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)
thus a in the_stable_subset_generated_by (X,A) by A22, A26; :: thesis: verum