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

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

let x be set ; :: 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 12;
(Product F,A) .: Y c= Y by A3, Lm30;
hence x in Y by A5, A7, A9; :: thesis: verum

end;

hence B c= Y by TARSKI:def 3; :: thesis: verum

end;

now

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

reconsider o = o as Element of O ;
reconsider F99 = <*o*> as FinSequence of O by A12, FINSEQ_1:95;
let y be set ; :: thesis: ( y in f .: B implies y in B )
assume y in f .: B ; :: thesis: y in B
then consider x being set such that
A13: x in dom f and
A14: x in B and
A15: y = f . x by FUNCT_1:def 12;
y in rng f by A13, A15, FUNCT_1:12;
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, Lm29
.= (Product F99,A) . ((Product F9,A) . x9) by A19, FUNCT_1:23
.= e by A11, A12, A15, A16, A18, Lm26 ;
hence y in B ; :: thesis: verum

end;

hence f .: B c= B by TARSKI:def 3; :: thesis: verum

end;

end;

end;

then A20: B is_stable_under_the_action_of A by Def1;

now

set F = <*> O;
let x be set ; :: 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:35 ;
then (Product (<*> O),A) . x9 = e ;
hence x in B ; :: thesis: verum

end;

then X c= B by TARSKI:def 3;
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