:: SCMYCIEL semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V268() Element of bool REAL

bool REAL is non empty V233() V267() subset-closed V329() V332() set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V268() set

bool omega is non empty non trivial non finite V233() V267() V268() subset-closed V329() V332() set

bool NAT is non empty non trivial non finite V233() V267() V268() subset-closed V329() V332() set

K226() is set

{} is functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-membered cardinal {} -element FinSequence-membered V83() ext-real non positive non negative V216() V233() subset-closed set

the functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-membered cardinal {} -element FinSequence-membered V83() ext-real non positive non negative V216() V233() subset-closed set is functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-membered cardinal {} -element FinSequence-membered V83() ext-real non positive non negative V216() V233() subset-closed set

{{}} is non empty trivial finite finite-membered 1 -element V233() V267() subset-closed V329() V332() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

{{}} * is functional non empty FinSequence-membered FinSequenceSet of {{}}

[:({{}} *),{{}}:] is non empty set

bool [:({{}} *),{{}}:] is non empty V233() V267() subset-closed V329() V332() set

K36(({{}} *),{{}}) is functional non empty set

COMPLEX is set

RAT is set

INT is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

{{},1} is non empty finite finite-membered set

K386(NAT) is non empty V235() V330() V331() set

[:NAT,REAL:] is set

bool [:NAT,REAL:] is non empty V233() V267() subset-closed V329() V332() set

1 -tuples_on NAT is FinSequenceSet of NAT

NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT

{ b

[:REAL,REAL:] is set

bool [:REAL,REAL:] is non empty V233() V267() subset-closed V329() V332() set

Z_2 is V48() V52() V96() V116() V121() V122() V123() V132() V134() V139() V140() L13()

the U1 of Z_2 is set

[:COMPLEX,COMPLEX:] is set

bool [:COMPLEX,COMPLEX:] is non empty V233() V267() subset-closed V329() V332() set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V233() V267() subset-closed V329() V332() set

[:[:REAL,REAL:],REAL:] is set

bool [:[:REAL,REAL:],REAL:] is non empty V233() V267() subset-closed V329() V332() set

[:RAT,RAT:] is set

bool [:RAT,RAT:] is non empty V233() V267() subset-closed V329() V332() set

[:[:RAT,RAT:],RAT:] is set

bool [:[:RAT,RAT:],RAT:] is non empty V233() V267() subset-closed V329() V332() set

[:INT,INT:] is set

bool [:INT,INT:] is non empty V233() V267() subset-closed V329() V332() set

[:[:INT,INT:],INT:] is set

bool [:[:INT,INT:],INT:] is non empty V233() V267() subset-closed V329() V332() set

[:NAT,NAT:] is non empty non trivial non finite V268() set

[:[:NAT,NAT:],NAT:] is non empty non trivial non finite V268() set

bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite V233() V267() V268() subset-closed V329() V332() set

bool (bool REAL) is non empty V233() V267() subset-closed V329() V332() set

3 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

0 is functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-membered cardinal {} -element FinSequence-membered V83() ext-real non positive non negative V216() V233() subset-closed Element of NAT

len {} is functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-membered cardinal {} -element FinSequence-membered V83() ext-real non positive non negative V216() V233() subset-closed set

K653(1,2) is V83() ext-real non negative V216() Element of RAT

n is set

G is set

[n,G] is non empty set

{n,G} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,G},{n}} is non empty finite finite-membered V267() V268() set

n is set

G is set

[n,G] is non empty set

{n,G} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,G},{n}} is non empty finite finite-membered V267() V268() set

n is set

G is set

[n,G] is non empty set

{n,G} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,G},{n}} is non empty finite finite-membered V267() V268() set

n is set

MG is set

S is set

G is set

[G,MG] is non empty set

{G,MG} is non empty finite set

{G} is non empty trivial finite 1 -element set

{{G,MG},{G}} is non empty finite finite-membered V267() V268() set

{n,[G,MG]} is non empty finite set

c

[c

{c

{c

{{c

{S,[c

n is set

len n is epsilon-transitive epsilon-connected ordinal cardinal set

G is set

S is set

c

MG is set

n is set

{n} is non empty trivial finite 1 -element set

singletons {n} is Element of bool the U1 of (bspace {n})

bspace {n} is V48() L15( Z_2 )

bool {n} is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

bspace-sum {n} is Relation-like [:(bool {n}),(bool {n}):] -defined bool {n} -valued Function-like non empty V14([:(bool {n}),(bool {n}):]) quasi_total finite Element of bool [:[:(bool {n}),(bool {n}):],(bool {n}):]

[:(bool {n}),(bool {n}):] is non empty finite set

[:[:(bool {n}),(bool {n}):],(bool {n}):] is non empty finite set

bool [:[:(bool {n}),(bool {n}):],(bool {n}):] is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

{} {n} is functional empty trivial proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-membered cardinal {} -element FinSequence-membered V83() ext-real non positive non negative V216() V233() subset-closed Element of bool {n}

bspace-scalar-mult {n} is Relation-like [: the U1 of Z_2,(bool {n}):] -defined bool {n} -valued Function-like V14([: the U1 of Z_2,(bool {n}):]) quasi_total Element of bool [:[: the U1 of Z_2,(bool {n}):],(bool {n}):]

[: the U1 of Z_2,(bool {n}):] is set

[:[: the U1 of Z_2,(bool {n}):],(bool {n}):] is set

bool [:[: the U1 of Z_2,(bool {n}):],(bool {n}):] is non empty V233() V267() subset-closed V329() V332() set

G15(Z_2,(bool {n}),(bspace-sum {n}),({} {n}),(bspace-scalar-mult {n})) is V142( Z_2 ) L15( Z_2 )

the U1 of (bspace {n}) is set

bool the U1 of (bspace {n}) is non empty V233() V267() subset-closed V329() V332() set

{ b

{{n}} is non empty trivial finite finite-membered 1 -element V267() V268() set

G is set

S is trivial finite Element of bool {n}

G is set

<*{}*> is Relation-like NAT -defined Function-like non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

G is set

rng n is finite set

n is non empty finite set

card n is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of omega

G is non empty finite finite-membered V267() V268() a_partition of n

card G is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of omega

proj G is Relation-like n -defined G -valued Function-like non empty V14(n) quasi_total finite Element of bool [:n,G:]

[:n,G:] is non empty finite set

bool [:n,G:] is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

S is set

c

(proj G) . S is set

(proj G) . c

MG is set

union {{}} is finite set

n is set

{n} is non empty trivial finite 1 -element set

{{},{n}} is non empty finite finite-membered set

union {{},{n}} is finite set

bool {n} is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

union (bool {n}) is finite set

n is set

bool n is non empty V233() V267() subset-closed V329() V332() set

G is Element of bool n

S is Element of G

{S} is non empty trivial finite 1 -element set

n is set

{ {n,[b

len { {n,[b

len n is epsilon-transitive epsilon-connected ordinal cardinal set

c

dom c

MG is set

n is set

c

c

[MG,n] is non empty set

{MG,n} is non empty finite set

{MG} is non empty trivial finite 1 -element set

{{MG,n},{MG}} is non empty finite finite-membered V267() V268() set

{n,[MG,n]} is non empty finite set

[n,n] is non empty set

{n,n} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,n},{n}} is non empty finite finite-membered V267() V268() set

{n,[n,n]} is non empty finite set

rng c

MG is set

n is set

c

[n,n] is non empty set

{n,n} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,n},{n}} is non empty finite finite-membered V267() V268() set

{n,[n,n]} is non empty finite set

MG is set

n is Element of n

[n,n] is non empty set

{n,n} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,n},{n}} is non empty finite finite-membered V267() V268() set

{n,[n,n]} is non empty finite set

c

n is set

bool n is non empty V233() V267() subset-closed V329() V332() set

G is Element of bool n

S is set

len S is epsilon-transitive epsilon-connected ordinal cardinal set

c

len c

G is Element of bool n

S is Element of bool n

c

len c

n is set

(n) is Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

union n is set

G is set

len G is epsilon-transitive epsilon-connected ordinal cardinal set

S is set

c

{S,c

G is set

S is set

{G,S} is non empty finite set

n is set

(n) is Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

card {G,S} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of omega

G is set

S is set

{G,S} is non empty finite set

n is set

(n) is Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

union n is set

c

MG is set

{c

n is set

G is set

(n) is Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

(G) is Element of bool G

bool G is non empty V233() V267() subset-closed V329() V332() set

S is set

len S is epsilon-transitive epsilon-connected ordinal cardinal set

n is finite set

union n is set

(n) is finite Element of bool n

bool n is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

{ {b

len { {b

card (n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

2 * (card (n)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of NAT

canFS (n) is Relation-like NAT -defined (n) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of (n)

the Relation-like NAT -defined (n) -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like FinSequence of (n) is Relation-like NAT -defined (n) -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like FinSequence of (n)

len (canFS (n)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of NAT

rng (canFS (n)) is finite set

H is set

E is set

S is set

C is set

EuG is set

{C,EuG} is non empty finite set

[EuG,(union n)] is non empty set

{EuG,(union n)} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,(union n)},{EuG}} is non empty finite finite-membered V267() V268() set

{C,[EuG,(union n)]} is non empty finite set

[C,(union n)] is non empty set

{C,(union n)} is non empty finite set

{C} is non empty trivial finite 1 -element set

{{C,(union n)},{C}} is non empty finite finite-membered V267() V268() set

{EuG,[C,(union n)]} is non empty finite set

{{C,[EuG,(union n)]},{EuG,[C,(union n)]}} is non empty finite finite-membered V267() V268() set

H is set

E is set

S is set

{E,S} is non empty finite set

[S,(union n)] is non empty set

{S,(union n)} is non empty finite set

{S} is non empty trivial finite 1 -element set

{{S,(union n)},{S}} is non empty finite finite-membered V267() V268() set

{E,[S,(union n)]} is non empty finite set

[E,(union n)] is non empty set

{E,(union n)} is non empty finite set

{E} is non empty trivial finite 1 -element set

{{E,(union n)},{E}} is non empty finite finite-membered V267() V268() set

{S,[E,(union n)]} is non empty finite set

{{E,[S,(union n)]},{S,[E,(union n)]}} is non empty finite finite-membered V267() V268() set

C is non empty finite finite-membered V267() V268() set

EuG is set

EuG is set

{EuG,EuG} is non empty finite set

[EuG,(union n)] is non empty set

{EuG,(union n)} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,(union n)},{EuG}} is non empty finite finite-membered V267() V268() set

{EuG,[EuG,(union n)]} is non empty finite set

[EuG,(union n)] is non empty set

{EuG,(union n)} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,(union n)},{EuG}} is non empty finite finite-membered V267() V268() set

{EuG,[EuG,(union n)]} is non empty finite set

{{EuG,[EuG,(union n)]},{EuG,[EuG,(union n)]}} is non empty finite finite-membered V267() V268() set

H is Relation-like Function-like set

dom H is set

E is set

(canFS (n)) * H is Relation-like finite set

rng ((canFS (n)) * H) is finite set

rng H is set

S is set

H . S is set

C is set

EuG is set

{C,EuG} is non empty finite set

[EuG,(union n)] is non empty set

{EuG,(union n)} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,(union n)},{EuG}} is non empty finite finite-membered V267() V268() set

{C,[EuG,(union n)]} is non empty finite set

[C,(union n)] is non empty set

{C,(union n)} is non empty finite set

{C} is non empty trivial finite 1 -element set

{{C,(union n)},{C}} is non empty finite finite-membered V267() V268() set

{EuG,[C,(union n)]} is non empty finite set

{{C,[EuG,(union n)]},{EuG,[C,(union n)]}} is non empty finite finite-membered V267() V268() set

E is Relation-like NAT -defined Function-like finite finite-yielding FinSequence-like FinSubsequence-like set

dom E is finite Element of bool NAT

dom (canFS (n)) is finite Element of bool NAT

len E is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of NAT

S is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V218() V219() V220() V221() FinSequence of NAT

len S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of NAT

dom S is finite Element of bool NAT

C is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

E . C is finite set

S . C is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

card (E . C) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

C is set

EuG is set

(canFS (n)) . C is set

(canFS (n)) . EuG is set

EuG is set

uG is set

{EuG,uG} is non empty finite set

se is set

sev is set

{se,sev} is non empty finite set

E . C is finite set

H . ((canFS (n)) . C) is set

E . EuG is finite set

H . ((canFS (n)) . EuG) is set

[uG,(union n)] is non empty set

{uG,(union n)} is non empty finite set

{uG} is non empty trivial finite 1 -element set

{{uG,(union n)},{uG}} is non empty finite finite-membered V267() V268() set

{EuG,[uG,(union n)]} is non empty finite set

[EuG,(union n)] is non empty set

{EuG,(union n)} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,(union n)},{EuG}} is non empty finite finite-membered V267() V268() set

{uG,[EuG,(union n)]} is non empty finite set

{{EuG,[uG,(union n)]},{uG,[EuG,(union n)]}} is non empty finite finite-membered V267() V268() set

[sev,(union n)] is non empty set

{sev,(union n)} is non empty finite set

{sev} is non empty trivial finite 1 -element set

{{sev,(union n)},{sev}} is non empty finite finite-membered V267() V268() set

{se,[sev,(union n)]} is non empty finite set

[se,(union n)] is non empty set

{se,(union n)} is non empty finite set

{se} is non empty trivial finite 1 -element set

{{se,(union n)},{se}} is non empty finite finite-membered V267() V268() set

{sev,[se,(union n)]} is non empty finite set

{{se,[sev,(union n)]},{sev,[se,(union n)]}} is non empty finite finite-membered V267() V268() set

csev is set

E . C is finite set

E . EuG is finite set

Union E is set

rng E is finite finite-membered set

union (rng E) is finite set

card (union (rng E)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

Sum S is V216() set

(len S) |-> 2 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like V218() V219() V220() V221() Element of (len S) -tuples_on NAT

(len S) -tuples_on NAT is FinSequenceSet of NAT

{ b

Seg (len S) is finite len S -element Element of bool NAT

K197((Seg (len S)),2) is Relation-like Seg (len S) -defined {2} -valued Function-like V14( Seg (len S)) quasi_total finite V218() V219() V220() V221() Element of bool [:(Seg (len S)),{2}:]

{2} is non empty trivial finite finite-membered 1 -element V267() V268() set

[:(Seg (len S)),{2}:] is finite set

bool [:(Seg (len S)),{2}:] is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

dom ((len S) |-> 2) is finite Element of bool NAT

C is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

E . C is finite set

(canFS (n)) . C is set

H . ((canFS (n)) . C) is set

EuG is set

EuG is set

{EuG,EuG} is non empty finite set

[EuG,(union n)] is non empty set

{EuG,(union n)} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,(union n)},{EuG}} is non empty finite finite-membered V267() V268() set

{EuG,[EuG,(union n)]} is non empty finite set

[EuG,(union n)] is non empty set

{EuG,(union n)} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,(union n)},{EuG}} is non empty finite finite-membered V267() V268() set

{EuG,[EuG,(union n)]} is non empty finite set

{{EuG,[EuG,(union n)]},{EuG,[EuG,(union n)]}} is non empty finite finite-membered V267() V268() set

S . C is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

card (E . C) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

((len S) |-> 2) . C is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

C is set

EuG is set

EuG is set

E . EuG is finite set

(canFS (n)) . EuG is set

H . ((canFS (n)) . EuG) is set

uG is set

se is set

{uG,se} is non empty finite set

[se,(union n)] is non empty set

{se,(union n)} is non empty finite set

{se} is non empty trivial finite 1 -element set

{{se,(union n)},{se}} is non empty finite finite-membered V267() V268() set

{uG,[se,(union n)]} is non empty finite set

[uG,(union n)] is non empty set

{uG,(union n)} is non empty finite set

{uG} is non empty trivial finite 1 -element set

{{uG,(union n)},{uG}} is non empty finite finite-membered V267() V268() set

{se,[uG,(union n)]} is non empty finite set

{{uG,[se,(union n)]},{se,[uG,(union n)]}} is non empty finite finite-membered V267() V268() set

C is set

EuG is Element of union n

EuG is Element of union n

[EuG,(union n)] is non empty set

{EuG,(union n)} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,(union n)},{EuG}} is non empty finite finite-membered V267() V268() set

{EuG,[EuG,(union n)]} is non empty finite set

{EuG,EuG} is non empty finite set

uG is set

(canFS (n)) . uG is set

H . ((canFS (n)) . uG) is set

[EuG,(union n)] is non empty set

{EuG,(union n)} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,(union n)},{EuG}} is non empty finite finite-membered V267() V268() set

{EuG,[EuG,(union n)]} is non empty finite set

{{EuG,[EuG,(union n)]},{EuG,[EuG,(union n)]}} is non empty finite finite-membered V267() V268() set

n is finite set

union n is set

(n) is finite Element of bool n

bool n is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

{ [b

len { [b

card (n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

2 * (card (n)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of NAT

{ {b

MG is set

n is Element of union n

H is Element of union n

[H,(union n)] is non empty set

{H,(union n)} is non empty finite set

{H} is non empty trivial finite 1 -element set

{{H,(union n)},{H}} is non empty finite finite-membered V267() V268() set

{n,[H,(union n)]} is non empty finite set

{n,H} is non empty finite set

[n,H] is non empty set

{n} is non empty trivial finite 1 -element set

{{n,H},{n}} is non empty finite finite-membered V267() V268() set

MG is set

n is Element of union n

H is Element of union n

[n,H] is non empty set

{n,H} is non empty finite set

{n} is non empty trivial finite 1 -element set

{{n,H},{n}} is non empty finite finite-membered V267() V268() set

E is set

S is Element of union n

C is Element of union n

[C,(union n)] is non empty set

{C,(union n)} is non empty finite set

{C} is non empty trivial finite 1 -element set

{{C,(union n)},{C}} is non empty finite finite-membered V267() V268() set

{S,[C,(union n)]} is non empty finite set

{S,C} is non empty finite set

[S,C] is non empty set

{S} is non empty trivial finite 1 -element set

{{S,C},{S}} is non empty finite finite-membered V267() V268() set

EuG is non empty set

EuG is Element of union n

uG is Element of union n

[uG,(union n)] is non empty set

{uG,(union n)} is non empty finite set

{uG} is non empty trivial finite 1 -element set

{{uG,(union n)},{uG}} is non empty finite finite-membered V267() V268() set

{EuG,[uG,(union n)]} is non empty finite set

[EuG,uG] is non empty set

{EuG,uG} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,uG},{EuG}} is non empty finite finite-membered V267() V268() set

[: { {b

bool [: { {b

E is Relation-like { {b

dom E is set

S is set

C is set

E . S is set

E . C is set

EuG is Element of union n

EuG is Element of union n

[EuG,(union n)] is non empty set

{EuG,(union n)} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,(union n)},{EuG}} is non empty finite finite-membered V267() V268() set

{EuG,[EuG,(union n)]} is non empty finite set

{EuG,EuG} is non empty finite set

uG is Element of union n

se is Element of union n

[se,(union n)] is non empty set

{se,(union n)} is non empty finite set

{se} is non empty trivial finite 1 -element set

{{se,(union n)},{se}} is non empty finite finite-membered V267() V268() set

{uG,[se,(union n)]} is non empty finite set

{uG,se} is non empty finite set

[EuG,EuG] is non empty set

{EuG} is non empty trivial finite 1 -element set

{{EuG,EuG},{EuG}} is non empty finite finite-membered V267() V268() set

[uG,se] is non empty set

{uG} is non empty trivial finite 1 -element set

{{uG,se},{uG}} is non empty finite finite-membered V267() V268() set

rng E is set

S is set

C is set

E . C is set

EuG is Element of union n

EuG is Element of union n

[EuG,(union n)] is non empty set

{EuG,(union n)} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,(union n)},{EuG}} is non empty finite finite-membered V267() V268() set

{EuG,[EuG,(union n)]} is non empty finite set

{EuG,EuG} is non empty finite set

[EuG,EuG] is non empty set

{EuG} is non empty trivial finite 1 -element set

{{EuG,EuG},{EuG}} is non empty finite finite-membered V267() V268() set

S is set

C is Element of union n

EuG is Element of union n

[C,EuG] is non empty set

{C,EuG} is non empty finite set

{C} is non empty trivial finite 1 -element set

{{C,EuG},{C}} is non empty finite finite-membered V267() V268() set

[EuG,(union n)] is non empty set

{EuG,(union n)} is non empty finite set

{EuG} is non empty trivial finite 1 -element set

{{EuG,(union n)},{EuG}} is non empty finite finite-membered V267() V268() set

{C,[EuG,(union n)]} is non empty finite set

E . {C,[EuG,(union n)]} is set

len { {b

n is finite set

(n) is finite Element of bool n

bool n is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

n is set

n is finite () set

union n is set

n is set

(n) is Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

G is set

len G is epsilon-transitive epsilon-connected ordinal cardinal set

n is set

union n is set

G is set

S is set

S is set

n is set

union n is set

len (union n) is epsilon-transitive epsilon-connected ordinal cardinal set

(n) is Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

S is set

c

MG is set

{c

n is set

{n} is non empty trivial finite 1 -element set

n is set

bool n is non empty V233() V267() subset-closed V329() V332() set

{ b

union { b

S is set

c

MG is finite Element of bool n

card MG is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

S is set

{S} is non empty trivial finite 1 -element set

card {S} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of omega

n is finite-membered set

G is set

n /\ G is set

S is set

n \ G is finite-membered Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

G is set

S is set

len S is epsilon-transitive epsilon-connected ordinal cardinal set

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

S is set

len S is epsilon-transitive epsilon-connected ordinal cardinal set

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

n is non empty V233() V267() subset-closed set

G is set

n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

G is finite-membered (n) set

S is finite Element of G

card S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

G is finite-membered (n) set

S is finite-membered (n) set

G \/ S is finite-membered set

c

len c

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

G is finite-membered (n) set

S is set

G /\ S is finite-membered set

c

len c

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

G \ S is finite-membered Element of bool G

bool G is non empty V233() V267() subset-closed V329() V332() set

c

len c

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

G is finite-membered (n) set

bool G is non empty V233() V267() subset-closed V329() V332() set

S is finite-membered Element of bool G

c

len c

n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

n is set

n is set

n is non empty finite-membered V233() V267() subset-closed (1) () set

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

bool (union n) is non empty V233() V267() subset-closed V329() V332() set

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

G is set

{G} is non empty trivial finite 1 -element set

S is set

n is set

{n} is non empty trivial finite 1 -element set

{{},{n}} is non empty finite finite-membered set

S is set

len S is epsilon-transitive epsilon-connected ordinal cardinal set

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

S is set

c

n is finite finite-membered set

union n is finite set

card (union n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

n is finite set

(n) is finite Element of bool n

bool n is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

card (n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

n is non empty finite finite-membered V233() V267() subset-closed (1) () set

(n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() set

union n is finite set

card (union n) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

card n is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of omega

singletons (union n) is Element of bool the U1 of (bspace (union n))

bspace (union n) is V48() L15( Z_2 )

bool (union n) is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

bspace-sum (union n) is Relation-like [:(bool (union n)),(bool (union n)):] -defined bool (union n) -valued Function-like non empty V14([:(bool (union n)),(bool (union n)):]) quasi_total finite Element of bool [:[:(bool (union n)),(bool (union n)):],(bool (union n)):]

[:(bool (union n)),(bool (union n)):] is non empty finite set

[:[:(bool (union n)),(bool (union n)):],(bool (union n)):] is non empty finite set

bool [:[:(bool (union n)),(bool (union n)):],(bool (union n)):] is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

{} (union n) is functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-membered cardinal {} -element FinSequence-membered V83() ext-real non positive non negative V216() V233() subset-closed Element of bool (union n)

bspace-scalar-mult (union n) is Relation-like [: the U1 of Z_2,(bool (union n)):] -defined bool (union n) -valued Function-like V14([: the U1 of Z_2,(bool (union n)):]) quasi_total Element of bool [:[: the U1 of Z_2,(bool (union n)):],(bool (union n)):]

[: the U1 of Z_2,(bool (union n)):] is set

[:[: the U1 of Z_2,(bool (union n)):],(bool (union n)):] is set

bool [:[: the U1 of Z_2,(bool (union n)):],(bool (union n)):] is non empty V233() V267() subset-closed V329() V332() set

G15(Z_2,(bool (union n)),(bspace-sum (union n)),({} (union n)),(bspace-scalar-mult (union n))) is V142( Z_2 ) L15( Z_2 )

the U1 of (bspace (union n)) is set

bool the U1 of (bspace (union n)) is non empty V233() V267() subset-closed V329() V332() set

{ b

len (singletons (union n)) is epsilon-transitive epsilon-connected ordinal cardinal set

S is set

c

MG is set

{MG} is non empty trivial finite 1 -element set

n is set

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

singletons (union n) is Element of bool the U1 of (bspace (union n))

bspace (union n) is V48() L15( Z_2 )

bool (union n) is non empty V233() V267() subset-closed V329() V332() set

bspace-sum (union n) is Relation-like [:(bool (union n)),(bool (union n)):] -defined bool (union n) -valued Function-like non empty V14([:(bool (union n)),(bool (union n)):]) quasi_total Element of bool [:[:(bool (union n)),(bool (union n)):],(bool (union n)):]

[:(bool (union n)),(bool (union n)):] is non empty set

[:[:(bool (union n)),(bool (union n)):],(bool (union n)):] is non empty set

bool [:[:(bool (union n)),(bool (union n)):],(bool (union n)):] is non empty V233() V267() subset-closed V329() V332() set

{} (union n) is functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-membered cardinal {} -element FinSequence-membered V83() ext-real non positive non negative V216() V233() subset-closed Element of bool (union n)

bspace-scalar-mult (union n) is Relation-like [: the U1 of Z_2,(bool (union n)):] -defined bool (union n) -valued Function-like V14([: the U1 of Z_2,(bool (union n)):]) quasi_total Element of bool [:[: the U1 of Z_2,(bool (union n)):],(bool (union n)):]

[: the U1 of Z_2,(bool (union n)):] is set

[:[: the U1 of Z_2,(bool (union n)):],(bool (union n)):] is set

bool [:[: the U1 of Z_2,(bool (union n)):],(bool (union n)):] is non empty V233() V267() subset-closed V329() V332() set

G15(Z_2,(bool (union n)),(bspace-sum (union n)),({} (union n)),(bspace-scalar-mult (union n))) is V142( Z_2 ) L15( Z_2 )

the U1 of (bspace (union n)) is set

bool the U1 of (bspace (union n)) is non empty V233() V267() subset-closed V329() V332() set

{ b

{{}} \/ (singletons (union n)) is non empty set

(n) is finite-membered (1) Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

({{}} \/ (singletons (union n))) \/ (n) is non empty set

G is set

S is finite set

card S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

c

{c

MG is Element of bool (union n)

G is set

S is set

S is Element of bool (union n)

c

{c

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

(n) is finite-membered (1) Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

G is set

singletons (union n) is Element of bool the U1 of (bspace (union n))

bspace (union n) is V48() L15( Z_2 )

bool (union n) is non empty V233() V267() subset-closed V329() V332() set

bspace-sum (union n) is Relation-like [:(bool (union n)),(bool (union n)):] -defined bool (union n) -valued Function-like non empty V14([:(bool (union n)),(bool (union n)):]) quasi_total Element of bool [:[:(bool (union n)),(bool (union n)):],(bool (union n)):]

[:(bool (union n)),(bool (union n)):] is non empty set

[:[:(bool (union n)),(bool (union n)):],(bool (union n)):] is non empty set

bool [:[:(bool (union n)),(bool (union n)):],(bool (union n)):] is non empty V233() V267() subset-closed V329() V332() set

{} (union n) is functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-membered cardinal {} -element FinSequence-membered V83() ext-real non positive non negative V216() V233() subset-closed Element of bool (union n)

bspace-scalar-mult (union n) is Relation-like [: the U1 of Z_2,(bool (union n)):] -defined bool (union n) -valued Function-like V14([: the U1 of Z_2,(bool (union n)):]) quasi_total Element of bool [:[: the U1 of Z_2,(bool (union n)):],(bool (union n)):]

[: the U1 of Z_2,(bool (union n)):] is set

[:[: the U1 of Z_2,(bool (union n)):],(bool (union n)):] is set

bool [:[: the U1 of Z_2,(bool (union n)):],(bool (union n)):] is non empty V233() V267() subset-closed V329() V332() set

G15(Z_2,(bool (union n)),(bspace-sum (union n)),({} (union n)),(bspace-scalar-mult (union n))) is V142( Z_2 ) L15( Z_2 )

the U1 of (bspace (union n)) is set

bool the U1 of (bspace (union n)) is non empty V233() V267() subset-closed V329() V332() set

{ b

{{}} \/ (singletons (union n)) is non empty set

({{}} \/ (singletons (union n))) \/ (n) is non empty set

S is Element of bool (union n)

c

{c

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

G is set

{G} is non empty trivial finite 1 -element set

{{},{G}} is non empty finite finite-membered set

(n) is finite-membered (1) Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

S is set

c

MG is set

{c

singletons (union n) is Element of bool the U1 of (bspace (union n))

bspace (union n) is V48() L15( Z_2 )

bool (union n) is non empty V233() V267() subset-closed V329() V332() set

bspace-sum (union n) is Relation-like [:(bool (union n)),(bool (union n)):] -defined bool (union n) -valued Function-like non empty V14([:(bool (union n)),(bool (union n)):]) quasi_total Element of bool [:[:(bool (union n)),(bool (union n)):],(bool (union n)):]

[:(bool (union n)),(bool (union n)):] is non empty set

[:[:(bool (union n)),(bool (union n)):],(bool (union n)):] is non empty set

bool [:[:(bool (union n)),(bool (union n)):],(bool (union n)):] is non empty V233() V267() subset-closed V329() V332() set

{} (union n) is functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-membered cardinal {} -element FinSequence-membered V83() ext-real non positive non negative V216() V233() subset-closed Element of bool (union n)

bspace-scalar-mult (union n) is Relation-like [: the U1 of Z_2,(bool (union n)):] -defined bool (union n) -valued Function-like V14([: the U1 of Z_2,(bool (union n)):]) quasi_total Element of bool [:[: the U1 of Z_2,(bool (union n)):],(bool (union n)):]

[: the U1 of Z_2,(bool (union n)):] is set

[:[: the U1 of Z_2,(bool (union n)):],(bool (union n)):] is set

bool [:[: the U1 of Z_2,(bool (union n)):],(bool (union n)):] is non empty V233() V267() subset-closed V329() V332() set

G15(Z_2,(bool (union n)),(bspace-sum (union n)),({} (union n)),(bspace-scalar-mult (union n))) is V142( Z_2 ) L15( Z_2 )

the U1 of (bspace (union n)) is set

bool the U1 of (bspace (union n)) is non empty V233() V267() subset-closed V329() V332() set

{ b

{{G}} is non empty trivial finite finite-membered 1 -element V267() V268() set

{{}} \/ (singletons (union n)) is non empty set

({{}} \/ (singletons (union n))) \/ (n) is non empty set

n is set

singletons n is Element of bool the U1 of (bspace n)

bspace n is V48() L15( Z_2 )

bool n is non empty V233() V267() subset-closed V329() V332() set

bspace-sum n is Relation-like [:(bool n),(bool n):] -defined bool n -valued Function-like non empty V14([:(bool n),(bool n):]) quasi_total Element of bool [:[:(bool n),(bool n):],(bool n):]

[:(bool n),(bool n):] is non empty set

[:[:(bool n),(bool n):],(bool n):] is non empty set

bool [:[:(bool n),(bool n):],(bool n):] is non empty V233() V267() subset-closed V329() V332() set

{} n is functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-membered cardinal {} -element FinSequence-membered V83() ext-real non positive non negative V216() V233() subset-closed Element of bool n

bspace-scalar-mult n is Relation-like [: the U1 of Z_2,(bool n):] -defined bool n -valued Function-like V14([: the U1 of Z_2,(bool n):]) quasi_total Element of bool [:[: the U1 of Z_2,(bool n):],(bool n):]

[: the U1 of Z_2,(bool n):] is set

[:[: the U1 of Z_2,(bool n):],(bool n):] is set

bool [:[: the U1 of Z_2,(bool n):],(bool n):] is non empty V233() V267() subset-closed V329() V332() set

G15(Z_2,(bool n),(bspace-sum n),({} n),(bspace-scalar-mult n)) is V142( Z_2 ) L15( Z_2 )

the U1 of (bspace n) is set

bool the U1 of (bspace n) is non empty V233() V267() subset-closed V329() V332() set

{ b

{{}} \/ (singletons n) is non empty set

S is set

c

MG is Element of bool n

n is set

{n} is non empty trivial finite 1 -element set

S is set

len S is epsilon-transitive epsilon-connected ordinal cardinal set

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

c

MG is set

{MG} is non empty trivial finite 1 -element set

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

S is non empty finite-membered V233() V267() subset-closed (1) () set

union S is set

(S) is finite-membered (1) Element of bool S

bool S is non empty V233() V267() subset-closed V329() V332() set

c

len c

MG is Element of bool n

n is set

{n} is non empty trivial finite 1 -element set

c

MG is set

n is Element of bool n

c

{c

MG is Element of bool n

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

bool (union n) is non empty V233() V267() subset-closed V329() V332() set

G is Element of union n

(n) is finite-membered (1) Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

{ b

c

MG is Element of union n

{G,MG} is non empty finite set

c

MG is Element of union n

{G,MG} is non empty finite set

n is Element of union n

{G,n} is non empty finite set

S is Element of bool (union n)

c

MG is set

{G,MG} is non empty finite set

MG is set

{G,MG} is non empty finite set

n is set

G is non empty finite-membered V233() V267() subset-closed (1) () set

union G is set

n is set

bool n is non empty V233() V267() subset-closed V329() V332() set

{ b

S is set

c

MG is finite Element of bool n

card MG is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

n is finite Element of bool n

card n is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

S is set

len S is epsilon-transitive epsilon-connected ordinal cardinal set

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

c

card c

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

card {} is functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-membered cardinal {} -element FinSequence-membered V83() ext-real non positive non negative V216() V233() subset-closed Element of omega

S is non empty finite-membered V233() V267() subset-closed (1) () set

union S is set

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

((union n)) is non empty finite-membered V233() V267() subset-closed (1) () ( union n)

bool (union n) is non empty V233() V267() subset-closed V329() V332() set

{ b

S is set

c

card c

MG is set

{MG} is non empty trivial finite 1 -element set

{MG,MG} is non empty finite set

MG is set

n is set

{MG,n} is non empty finite set

S is set

c

card c

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

n is finite set

(n) is non empty finite-membered V233() V267() subset-closed (1) () (n)

bool n is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

{ b

S is set

c

card c

n is set

(n) is non empty finite-membered V233() V267() subset-closed (1) () (n)

bool n is non empty V233() V267() subset-closed V329() V332() set

{ b

G is set

{G} is non empty trivial finite 1 -element set

card {G} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of omega

n is set

(n) is non empty finite-membered V233() V267() subset-closed (1) () (n)

bool n is non empty V233() V267() subset-closed V329() V332() set

{ b

G is set

S is set

{G,S} is non empty finite set

card {G,S} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of omega

({}) is non empty finite finite-membered V233() V267() subset-closed (1) () ( {} )

bool {} is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

{ b

n is set

G is set

{n,G} is non empty finite set

n is set

{n} is non empty trivial finite 1 -element set

({n}) is non empty finite finite-membered V233() V267() subset-closed (1) () ({n})

bool {n} is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

{ b

{{},{n}} is non empty finite finite-membered set

G is set

S is trivial finite Element of bool {n}

card S is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

union ({n}) is finite set

G is set

n is set

G is set

{n,G} is non empty finite set

({n,G}) is non empty finite finite-membered V233() V267() subset-closed (1) () ({n,G})

bool {n,G} is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

{ b

{n} is non empty trivial finite 1 -element set

{G} is non empty trivial finite 1 -element set

{{},{n},{G},{n,G}} is non empty finite set

S is set

c

card c

union ({n,G}) is finite set

card {n,G} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of omega

S is set

n is set

G is set

(n) is non empty finite-membered V233() V267() subset-closed (1) () (n)

bool n is non empty V233() V267() subset-closed V329() V332() set

{ b

(G) is non empty finite-membered V233() V267() subset-closed (1) () (G)

bool G is non empty V233() V267() subset-closed V329() V332() set

{ b

S is set

c

card c

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

G is set

{G} is non empty trivial finite 1 -element set

({G}) is non empty finite finite-membered V233() V267() subset-closed (1) () ({G})

bool {G} is non empty finite finite-membered V233() V267() subset-closed V329() V332() set

{ b

{{},{G}} is non empty finite finite-membered set

n is non empty finite-membered V233() V267() subset-closed (1) () set

bool n is non empty V233() V267() subset-closed V329() V332() set

G is finite-membered (1) Element of bool n

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

((union n)) is non empty finite-membered V233() V267() subset-closed (1) () ( union n)

bool (union n) is non empty V233() V267() subset-closed V329() V332() set

{ b

(n) is finite-membered (1) Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

((union n)) \ (n) is finite-membered (1) Element of bool ((union n))

bool ((union n)) is non empty V233() V267() subset-closed V329() V332() set

c

MG is set

{c

c

MG is set

n is set

len n is epsilon-transitive epsilon-connected ordinal cardinal set

H is finite set

card H is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real positive non negative V216() Element of NAT

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

((union n)) is non empty finite-membered V233() V267() subset-closed (1) () ( union n)

bool (union n) is non empty V233() V267() subset-closed V329() V332() set

{ b

(n) is finite-membered (1) Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

((union n)) \ (n) is finite-membered (1) Element of bool ((union n))

bool ((union n)) is non empty V233() V267() subset-closed V329() V332() set

union (((union n)) \ (n)) is set

S is set

{S} is non empty trivial finite 1 -element set

{S,S} is non empty finite set

union ((union n)) is set

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

(n) is finite-membered (1) Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

((union n)) is non empty finite-membered V233() V267() subset-closed (1) () ( union n)

bool (union n) is non empty V233() V267() subset-closed V329() V332() set

{ b

((union n)) \ (n) is finite-membered (1) Element of bool ((union n))

bool ((union n)) is non empty V233() V267() subset-closed V329() V332() set

((((union n)) \ (n))) is finite-membered (1) Element of bool (((union n)) \ (n))

bool (((union n)) \ (n)) is non empty V233() V267() subset-closed V329() V332() set

G is set

S is set

{G,S} is non empty finite set

G is non empty finite-membered V233() V267() subset-closed (1) () set

n is non empty finite-membered V233() V267() subset-closed (1) () set

union n is set

((union n)) is non empty finite-membered V233() V267() subset-closed (1) () ( union n)

bool (union n) is non empty V233() V267() subset-closed V329() V332() set

{ b

(n) is finite-membered (1) Element of bool n

bool n is non empty V233() V267() subset-closed V329() V332() set

((union n)) \ (n) is finite-membered (1) Element of bool ((union n))

bool ((union n)) is non empty V233() V267() subset-closed V329() V332() set

union G is set

((union G)) is non empty finite-membered V233() V267() subset-closed (1) () ( union G)

bool (union G) is non empty V233() V267() subset-closed V329() V332() set

{ b

(G) is finite-membered (1) Element of bool G

bool G is non empty V233() V267() subset-closed V329() V332()