let O be set ; 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 ; 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; 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; 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; ( 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 S1[ 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 : S1[e] } ;
reconsider B = { e where e is Element of E : S1[e] } as Subset of E from DOMAIN_1:sch 7();
assume A1:
not X is empty
; ( 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 for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
B c= Ylet Y be
Subset of
E;
( 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
;
( X c= Y implies B c= Y )assume A4:
X c= Y
;
B c= Ynow for x being object st x in B holds
x in Ylet x be
object ;
( x in B implies x in Y )assume
x in B
;
x in Ythen 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;
verum end; hence
B c= Y
;
verum end;
now for o being Element of O
for f being Function of E,E st o in O & f = A . o holds
f .: B c= Blet o be
Element of
O;
for f being Function of E,E st o in O & f = A . o holds
b3 .: B c= Blet f be
Function of
E,
E;
( o in O & f = A . o implies b2 .: B c= B )assume A10:
o in O
;
( f = A . o implies b2 .: B c= B )assume A11:
f = A . o
;
b2 .: B c= Bper cases
( O = {} or O <> {} )
;
suppose A12:
O <> {}
;
b2 .: B c= Bnow for y being object st y in f .: B holds
y in Breconsider o =
o as
Element of
O ;
reconsider F99 =
<*o*> as
FinSequence of
O by A12, FINSEQ_1:74;
let y be
object ;
( y in f .: B implies y in B )assume
y in f .: B
;
y in Bthen 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
;
verum end; hence
f .: B c= B
;
verum end; end; end;
then A20:
B is_stable_under_the_action_of A
;
then
X c= B
;
then A22:
B = the_stable_subset_generated_by (X,A)
by A20, A2, Def2;
given F being FinSequence of O, x being Element of X such that A26:
(Product (F,A)) . x = a
; a in the_stable_subset_generated_by (X,A)
thus
a in the_stable_subset_generated_by (X,A)
by A22, A26; verum