let O be set ; :: thesis:
let E be non empty set ; :: thesis:
let A be Action of O,E; :: thesis:
let X be Subset of E; :: thesis:
let a be Element of E; :: thesis:
assume A1: not X is empty ; :: thesis:
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();

let x be set ; :: thesis:
assume A2: x in X ; :: thesis:
set F = <*> O;
len (<*> O) = 0 ;
then A3: (Product (<*> O),A) . x = (id E) . x by Def3
.= x by A2, FUNCT_1:35 ;
reconsider e = x as Element of E by A2;
reconsider x' = e as Element of X by A2;
(Product (<*> O),A) . x' = e by A3;
hence x in B ; :: thesis:

end;

then A4: X c= B by TARSKI:def 3;

let o be Element of O; :: thesis:
let f be Function of E,E; :: thesis:
assume A5: o in O ; :: thesis:
assume A6: f = A . o ; :: thesis:

per cases ;

suppose O = {} ; :: thesis:

hence f .: B c= B by A5; :: thesis:

end;

suppose A7: O <> {} ; :: thesis:

let y be set ; :: thesis:
assume y in f .: B ; :: thesis:
then consider x being set such that
A8: ( x in dom f & x in B & y = f . x ) by FUNCT_1:def 12;
consider e' being Element of E such that
A9: ( e' = x & ex F' being FinSequence of O ex x' being Element of X st (Product F',A) . x' = e' ) by A8;
consider F' being FinSequence of O, x' being Element of X such that
A10: (Product F',A) . x' = e' by A9;
reconsider o = o as Element of O ;
reconsider F'' = <*o*> as FinSequence of O by A7, FINSEQ_1:95;
reconsider F = F'' ^ F' as FinSequence of O ;
y in rng f by A8, FUNCT_1:12;
then reconsider e = y as Element of E ;
x' in X by A1;
then x' in E ;
then A11: x' in dom (Product F',A) by FUNCT_2:def 1;
(Product F,A) . x' = ((Product F'',A) * (Product F',A)) . x' by A7, Lm29
.= (Product F'',A) . ((Product F',A) . x') by A11, FUNCT_1:23
.= e by A6, A7, A8, A9, A10, Lm26 ;
hence y in B ; :: thesis:

end;

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

end;

then A12: B is_stable_under_the_action_of A by Def1;

let Y be Subset of E; :: thesis:
assume A13: Y is_stable_under_the_action_of A ; :: thesis:
assume A14: X c= Y ; :: thesis:

let x be set ; :: thesis:
assume x in B ; :: thesis:
then consider e being Element of E such that
A15: ( x = e & ex F being FinSequence of O ex x' being Element of X st (Product F,A) . x' = e ) ;
consider F being FinSequence of O, x' being Element of X such that
A16: (Product F,A) . x' = e by A15;
A17: x' in X by A1;
then x' in E ;
then A18: x' in dom (Product F,A) by FUNCT_2:def 1;
A19: (Product F,A) .: Y c= Y by A13, Lm30;
(Product F,A) . x' in (Product F,A) .: Y by A14, A17, A18, FUNCT_1:def 12;
hence x in Y by A15, A16, A19; :: thesis:

end;

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

end;

then A20: B = the_stable_subset_generated_by X,A by A4, A12, Def2;

hereby :: thesis:

assume a in the_stable_subset_generated_by X,A ; :: thesis:
then consider e being Element of E such that
A21: ( a = e & ex F being FinSequence of O ex x being Element of X st (Product F,A) . x = e ) by A20;
consider F being FinSequence of O, x being Element of X such that
A22: (Product F,A) . x = e by A21;
take F = F; :: thesis:
take x = x; :: thesis:
thus (Product F,A) . x = a by A21, A22; :: thesis:

end;

given F being FinSequence of O, x being Element of X such that A23: (Product F,A) . x = a ; :: thesis:
thus a in the_stable_subset_generated_by X,A by A20, A23; :: thesis: