:: 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₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b₁ = 1 } is set
[: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₄ is set
[c₄,MG] is non empty set
{c₄,MG} is non empty finite set
{c₄} is non empty trivial finite 1 -element set
{{c₄,MG},{c₄}} is non empty finite finite-membered V267() V268() set
{S,[c₄,MG]} is non empty finite set
n is set
len n is epsilon-transitive epsilon-connected ordinal cardinal set
G is set
S is set
c₄ is set
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₁ where b₁ is Element of bool {n} : b₁ is 1 -element } is set
{{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₄ is set
(proj G) . S is set
(proj G) . c₄ is set
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₁,n]} where b₁ is Element of n : b₁ in n } is set
len { {n,[b₁,n]} where b₁ is Element of n : b₁ in n } is epsilon-transitive epsilon-connected ordinal cardinal set
len n is epsilon-transitive epsilon-connected ordinal cardinal set
c₄ is Relation-like Function-like set
dom c₄ is set
MG is set
n is set
c₄ . MG is set
c₄ . n is set
[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₄ is set
MG is set
n is set
c₄ . n is 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
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
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₄ is set
len c₄ is epsilon-transitive epsilon-connected ordinal cardinal set
G is Element of bool n
S is Element of bool n
c₄ is set
len c₄ is epsilon-transitive epsilon-connected ordinal cardinal 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
G is set
len G is epsilon-transitive epsilon-connected ordinal cardinal set
S is set
c₄ is set
{S,c₄} is non empty finite set
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₄ is set
MG is set
{c₄,MG} is non empty finite set
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₁,[b₂,(union n)]} where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } is set
len { {b₁,[b₂,(union n)]} where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } is epsilon-transitive epsilon-connected ordinal cardinal set
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₁ where b₁ is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b₁ = len S } is set
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₁,b₂] where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } is set
len { [b₁,b₂] where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } is epsilon-transitive epsilon-connected ordinal cardinal set
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₁,[b₂,(union n)]} where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } is set
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₁,[b₂,(union n)]} where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } , { [b₁,b₂] where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } :] is set
bool [: { {b₁,[b₂,(union n)]} where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } , { [b₁,b₂] where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } :] is non empty V233() V267() subset-closed V329() V332() set
E is Relation-like { {b₁,[b₂,(union n)]} where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } -defined { [b₁,b₂] where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } -valued Function-like quasi_total Element of bool [: { {b₁,[b₂,(union n)]} where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } , { [b₁,b₂] where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } :]
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₁,[b₂,(union n)]} where b₁, b₂ is Element of union n : {b₁,b₂} in (n) } is epsilon-transitive epsilon-connected ordinal cardinal set
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₄ is set
MG is set
{c₄,MG} is non empty finite set
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₁ where b₁ is finite Element of bool n : card b₁ <= 2 } is set
union { b₁ where b₁ is finite Element of bool n : card b₁ <= 2 } is set
S is set
c₄ is set
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₄ is set
len c₄ 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
G is finite-membered (n) set
S is set
G /\ S is finite-membered set
c₄ is set
len c₄ 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
G \ S is finite-membered Element of bool G
bool G is non empty V233() V267() subset-closed V329() V332() set
c₄ is set
len c₄ 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
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₄ is set
len c₄ 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 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₄ is set
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₁ where b₁ is Element of bool (union n) : b₁ is 1 -element } is set
len (singletons (union n)) is epsilon-transitive epsilon-connected ordinal cardinal set
S is set
c₄ is finite Element of bool (union n)
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₁ where b₁ is Element of bool (union n) : b₁ is 1 -element } is set
{{}} \/ (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₄ is set
{c₄} is non empty trivial finite 1 -element set
MG is Element of bool (union n)
G is set
S is set
S is Element of bool (union n)
c₄ is set
{c₄} is non empty trivial finite 1 -element set
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₁ where b₁ is Element of bool (union n) : b₁ is 1 -element } is set
{{}} \/ (singletons (union n)) is non empty set
({{}} \/ (singletons (union n))) \/ (n) is non empty set
S is Element of bool (union n)
c₄ is set
{c₄} is non empty trivial finite 1 -element 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
{{},{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₄ is set
MG is set
{c₄,MG} is non empty finite 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₁ where b₁ is Element of bool (union n) : b₁ is 1 -element } is set
{{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₁ where b₁ is Element of bool n : b₁ is 1 -element } is set
{{}} \/ (singletons n) is non empty set
S is set
c₄ is set
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₄ is Element of bool n
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₄ is set
len c₄ is epsilon-transitive epsilon-connected ordinal cardinal set
MG is Element of bool n
n is set
{n} is non empty trivial finite 1 -element set
c₄ is set
MG is set
n is Element of bool n
c₄ is set
{c₄} is non empty trivial finite 1 -element set
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₁ where b₁ is Element of union n : {G,b₁} in (n) } is set
c₄ is set
MG is Element of union n
{G,MG} is non empty finite set
c₄ is Element of bool (union n)
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₄ is Element of bool (union n)
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₁ where b₁ is finite Element of bool n : card b₁ <= 2 } is set
S is set
c₄ is set
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₄ is finite Element of bool n
card c₄ 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
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₁ where b₁ is finite Element of bool (union n) : card b₁ <= 2 } is set
S is set
c₄ is finite Element of bool (union n)
card c₄ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega
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₄ is finite set
card c₄ 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 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₁ where b₁ is finite Element of bool n : card b₁ <= 2 } is set
S is set
c₄ is finite Element of bool n
card c₄ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real 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₁ where b₁ is finite Element of bool n : card b₁ <= 2 } is set
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₁ where b₁ is finite Element of bool n : card b₁ <= 2 } is set
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₁ where b₁ is finite Element of bool {} : card b₁ <= 2 } is set
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₁ where b₁ is finite Element of bool {n} : card b₁ <= 2 } is set
{{},{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₁ where b₁ is finite Element of bool {n,G} : card b₁ <= 2 } is set
{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₄ is finite Element of bool {n,G}
card c₄ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega
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₁ where b₁ is finite Element of bool n : card b₁ <= 2 } is set
(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₁ where b₁ is finite Element of bool G : card b₁ <= 2 } is set
S is set
c₄ is finite Element of bool n
card c₄ is epsilon-transitive epsilon-connected ordinal natural finite cardinal V83() ext-real non negative V216() Element of omega
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₁ where b₁ is finite Element of bool {G} : card b₁ <= 2 } is set
{{},{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₁ where b₁ is finite Element of bool (union n) : card b₁ <= 2 } 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)) \ (n) is finite-membered (1) Element of bool ((union n))
bool ((union n)) is non empty V233() V267() subset-closed V329() V332() set
c₄ is set
MG is set
{c₄,MG} is non empty finite set
c₄ is non empty set
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₁ where b₁ is finite Element of bool (union n) : card b₁ <= 2 } 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)) \ (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₁ where b₁ is finite Element of bool (union n) : card b₁ <= 2 } is 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 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₁ where b₁ is finite Element of bool (union n) : card b₁ <= 2 } 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)) \ (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₁ where b₁ is finite Element of bool (union G) : card b₁ <= 2 } is set
(G) is finite-membered (1) Element of bool G
bool G is non empty V233() V267() subset-closed V329() V332()