REAL is non empty non trivial non finite set
NAT is non empty non trivial V29() V30() V31() non finite cardinal limit_cardinal countable denumerable Element of bool REAL
bool REAL is non empty non trivial non finite set
NAT is non empty non trivial V29() V30() V31() non finite cardinal limit_cardinal countable denumerable set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite set
RAT is non empty non trivial non finite set
INT is non empty non trivial non finite set
[:NAT,REAL:] is non empty non trivial Relation-like non finite set
bool [:NAT,REAL:] is non empty non trivial non finite set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like non finite set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:REAL,REAL:] is non empty non trivial Relation-like non finite set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is non empty non trivial Relation-like non finite set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like non finite set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is non empty non trivial Relation-like non finite set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is non empty non trivial Relation-like non finite set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is non empty non trivial Relation-like non finite set
[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like non finite set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
BOOLEAN is non empty set
1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
[:1,1:] is non empty Relation-like finite countable set
bool [:1,1:] is non empty finite V40() countable set
[:[:1,1:],1:] is non empty Relation-like finite countable set
bool [:[:1,1:],1:] is non empty finite V40() countable set
[:[:1,1:],REAL:] is non empty non trivial Relation-like non finite set
bool [:[:1,1:],REAL:] is non empty non trivial non finite set
2 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
[:2,2:] is non empty Relation-like finite countable set
[:[:2,2:],REAL:] is non empty non trivial Relation-like non finite set
bool [:[:2,2:],REAL:] is non empty non trivial non finite set
TOP-REAL 2 is V177() L15()
the carrier of (TOP-REAL 2) is set
{} is empty ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support set
3 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
0 is empty ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support Element of NAT
proj1 {} is empty ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support set
proj2 {} is empty trivial with_non-empty_elements ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support set
Seg 1 is non empty trivial finite 1 -element countable Element of bool NAT
FALSE is boolean Element of BOOLEAN
<*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
<*1*> is non empty trivial Relation-like NAT -defined NAT -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support FinSequence of NAT
X is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
F is non empty set
K is Relation-like NAT -defined F -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of F
len K is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dom K is finite X -element countable Element of bool NAT
Seg X is finite X -element countable Element of bool NAT
F is non empty set
X is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
X -tuples_on F is non empty functional FinSequence-membered FinSequenceSet of F
F * is non empty functional FinSequence-membered FinSequenceSet of F
{ b1 where b1 is Relation-like NAT -defined F -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of F * : len b1 = X } is set
K is Relation-like NAT -defined F -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support Element of X -tuples_on F
len K is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dom K is finite X -element countable Element of bool NAT
Seg X is finite X -element countable Element of bool NAT
X is set
F is set
bool F is non empty set
bool (bool F) is non empty set
K is finite countable Element of bool (bool F)
Intersect K is Element of bool F
dcF is set
S is set
{dcF} is non empty trivial finite 1 -element countable set
S \/ {dcF} is non empty set
ck is Element of bool (bool F)
S is Element of bool (bool F)
ck \/ S is Element of bool (bool F)
Intersect (ck \/ S) is Element of bool F
Intersect ck is Element of bool F
Intersect S is Element of bool F
(Intersect ck) /\ (Intersect S) is Element of bool F
B is Element of bool F
(Intersect ck) /\ B is Element of bool F
m is Element of bool (bool F)
Intersect m is Element of bool F
dcF is Element of bool (bool F)
Intersect dcF is Element of bool F
[{},{}] is V21() set
{{},{}} is non empty functional finite V40() countable set
{{}} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
{{{},{}},{{}}} is non empty finite V40() countable set
{[{},{}]} is non empty trivial Relation-like Function-like constant finite 1 -element countable finite-support set
F is Relation-like set
field F is set
K is set
[K,K] is V21() set
{K,K} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,K},{K}} is non empty finite V40() countable set
K is set
dcF is set
[K,dcF] is V21() set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
[dcF,K] is V21() set
{dcF,K} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,K},{dcF}} is non empty finite V40() countable set
K is set
dcF is set
S is set
[K,dcF] is V21() set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
[dcF,S] is V21() set
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
[K,S] is V21() set
{K,S} is non empty finite countable set
{{K,S},{K}} is non empty finite V40() countable set
X is non empty Relation-like antisymmetric transitive set
field X is set
bool (field X) is non empty set
F is finite countable Element of bool (field X)
[:(field X),(field X):] is Relation-like set
bool [:(field X),(field X):] is non empty set
K is Relation-like field X -defined field X -valued Element of bool [:(field X),(field X):]
RelStr(# (field X),K #) is strict RelStr
the carrier of RelStr(# (field X),K #) is set
the InternalRel of RelStr(# (field X),K #) is Relation-like the carrier of RelStr(# (field X),K #) -defined the carrier of RelStr(# (field X),K #) -valued Element of bool [: the carrier of RelStr(# (field X),K #), the carrier of RelStr(# (field X),K #):]
[: the carrier of RelStr(# (field X),K #), the carrier of RelStr(# (field X),K #):] is Relation-like set
bool [: the carrier of RelStr(# (field X),K #), the carrier of RelStr(# (field X),K #):] is non empty set
ck is Element of the carrier of RelStr(# (field X),K #)
B is Element of the carrier of RelStr(# (field X),K #)
m is Element of the carrier of RelStr(# (field X),K #)
[B,m] is V21() set
{B,m} is non empty finite countable set
{B} is non empty trivial finite 1 -element countable set
{{B,m},{B}} is non empty finite V40() countable set
[ck,B] is V21() set
{ck,B} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
[ck,m] is V21() set
{ck,m} is non empty finite countable set
{{ck,m},{ck}} is non empty finite V40() countable set
ck is Element of the carrier of RelStr(# (field X),K #)
B is Element of the carrier of RelStr(# (field X),K #)
[B,ck] is V21() set
{B,ck} is non empty finite countable set
{B} is non empty trivial finite 1 -element countable set
{{B,ck},{B}} is non empty finite V40() countable set
[ck,B] is V21() set
{ck,B} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
bool the carrier of RelStr(# (field X),K #) is non empty set
ck is non empty transitive antisymmetric RelStr
the carrier of ck is non empty set
B is finite countable Element of bool the carrier of RelStr(# (field X),K #)
the InternalRel of ck is Relation-like the carrier of ck -defined the carrier of ck -valued Element of bool [: the carrier of ck, the carrier of ck:]
[: the carrier of ck, the carrier of ck:] is non empty Relation-like set
bool [: the carrier of ck, the carrier of ck:] is non empty set
m is Element of the carrier of ck
P is Element of F
x9 is set
[P,x9] is V21() set
{P,x9} is non empty finite countable set
{P} is non empty trivial finite 1 -element countable set
{{P,x9},{P}} is non empty finite V40() countable set
F1() is set
bool F1() is non empty set
X is Element of bool F1()
F is Element of bool F1()
K is set
X is set
bool X is non empty set
F is Relation-like set
K is set
dcF is set
dcF is Element of bool X
S is set
X is non empty set
bool X is non empty set
{ b1 where b1 is Element of X : (b1,X) } is set
K is set
dcF is Element of X
K is Element of bool X
dcF is set
S is Element of X
F1() is non empty finite countable set
{ b1 where b1 is Element of F1() : a1 c= b1 } is set
X is set
{ b1 where b1 is Element of F1() : X c= b1 } is set
F is set
K is Element of F1()
F is finite countable set
card F is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dcF is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
K is Element of F1()
{ b1 where b1 is Element of F1() : K c= b1 } is set
card H1(K) is V29() V30() V31() cardinal set
K is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable set
dcF is Element of F1()
{ b1 where b1 is Element of F1() : dcF c= b1 } is set
card { b1 where b1 is Element of F1() : dcF c= b1 } is V29() V30() V31() cardinal set
dcF is Element of F1()
{ b1 where b1 is Element of F1() : dcF c= b1 } is set
card H1(dcF) is V29() V30() V31() cardinal set
S is set
S is Element of F1()
S is set
ck is set
S /\ ck is set
{ b1 where b1 is Element of F1() : S c= b1 } is set
B is set
m is Element of F1()
{ b1 where b1 is Element of F1() : ck c= b1 } is set
m is set
P is Element of F1()
m is finite countable set
S is finite countable set
y9 is set
P is Element of F1()
a is Element of F1()
P is Element of F1()
y9 is Element of F1()
card S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
card m is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
B is finite countable set
y9 is set
x9 is Element of F1()
a is Element of F1()
x9 is Element of F1()
y9 is Element of F1()
card B is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
X is non empty finite countable set
bool X is non empty finite V40() countable set
F is Element of X
K is set
dcF is set
S is non empty finite countable Element of bool X
meet S is set
S is non empty finite countable Element of bool X
meet S is set
S is non empty finite countable Element of bool X
meet S is set
S is non empty finite countable Element of bool X
meet S is set
S \/ S is non empty finite countable Element of bool X
ck is non empty finite countable Element of bool X
K /\ dcF is set
B is non empty finite countable Element of bool X
meet B is set
m is set
B is non empty finite countable Element of bool X
meet B is set
K is set
{K} is non empty trivial finite 1 -element countable set
dcF is non empty finite countable Element of bool X
meet dcF is set
S is set
X is set
bool X is non empty set
bool (bool X) is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
{X} is non empty trivial finite 1 -element countable set
K is Element of bool (bool X)
dcF is set
S is set
dcF /\ S is set
X is set
bool X is non empty set
bool (bool X) is non empty set
F is non empty Element of bool (bool X)
K is Element of F
dcF is finite countable Element of bool (bool X)
Intersect dcF is Element of bool X
S is set
S is set
{S} is non empty trivial finite 1 -element countable set
S \/ {S} is non empty set
ck is Element of F
B is Element of F
ck /\ B is Element of bool X
ck is Element of bool (bool X)
Intersect ck is Element of bool X
ck is Element of bool (bool X)
Intersect ck is Element of bool X
{S} is non empty trivial finite 1 -element countable set
S \/ {S} is non empty set
B is Element of bool (bool X)
Intersect B is Element of bool X
meet B is Element of bool X
S \/ B is set
m is non empty Element of bool (bool X)
Intersect m is Element of bool X
meet m is Element of bool X
meet S is set
(meet S) /\ (meet B) is Element of bool X
meet ck is Element of bool X
ck is Element of F
B is Element of F
ck /\ B is Element of bool X
m is Element of bool (bool X)
Intersect m is Element of bool X
S is Element of F
S is Element of F
S /\ S is Element of bool X
ck is Element of bool (bool X)
Intersect ck is Element of bool X
X is non empty set
K is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
F is non empty set
K -tuples_on F is non empty functional FinSequence-membered FinSequenceSet of F
F * is non empty functional FinSequence-membered FinSequenceSet of F
{ b1 where b1 is Relation-like NAT -defined F -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of F * : len b1 = K } is set
[:X,(K -tuples_on F):] is non empty Relation-like set
bool [:X,(K -tuples_on F):] is non empty set
dcF is Relation-like X -defined K -tuples_on F -valued Function-like V24(X,K -tuples_on F) Function-yielding V28() Element of bool [:X,(K -tuples_on F):]
S is set
proj1 dcF is set
dcF . S is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
dom dcF is Element of bool X
bool X is non empty set
X is Relation-like Function-like Function-yielding V28() FinSequence-yielding set
F is set
X . F is Relation-like Function-like set
proj1 X is set
proj1 X is set
proj1 X is set
X is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
Seg X is finite X -element countable Element of bool NAT
F is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
K is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dcF is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
len dcF is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dom dcF is finite countable Element of bool NAT
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
X -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b1 where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN * : len b1 = X } is set
S is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support Element of X -tuples_on BOOLEAN
S is set
S . S is set
F /. S is boolean Element of BOOLEAN
K /. S is boolean Element of BOOLEAN
(F /. S) '&' (K /. S) is boolean Element of BOOLEAN
K161((F /. S),(K /. S)) is set
dcF is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom dcF is finite X -element countable Element of bool NAT
dom S is finite X -element countable Element of bool NAT
S is set
dcF . S is set
F /. S is boolean Element of BOOLEAN
K /. S is boolean Element of BOOLEAN
(F /. S) '&' (K /. S) is boolean Element of BOOLEAN
K161((F /. S),(K /. S)) is set
S . S is set
dcF is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
ck is set
dcF . ck is set
S /. ck is boolean Element of BOOLEAN
S /. ck is boolean Element of BOOLEAN
(S /. ck) '&' (S /. ck) is boolean Element of BOOLEAN
K161((S /. ck),(S /. ck)) is set
X is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
X -tuples_on BOOLEAN is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
{ b1 where b1 is Relation-like NAT -defined BOOLEAN -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN * : len b1 = X } is set
X -BinarySequence 0 is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
F is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support Element of X -tuples_on BOOLEAN
(X,(X -BinarySequence 0),F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom (X -BinarySequence 0) is finite X -element countable Element of bool NAT
Seg X is finite X -element countable Element of bool NAT
dom (X,(X -BinarySequence 0),F) is finite X -element countable Element of bool NAT
S is set
0* X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of REAL X
REAL X is functional FinSequence-membered FinSequenceSet of REAL
X |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like Function-yielding V28() finite X -element FinSequence-like FinSubsequence-like Cardinal-yielding countable FinSequence-yielding finite-support Element of X -tuples_on NAT
X -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of NAT * : len b1 = X } is set
(Seg X) --> 0 is Relation-like Seg X -defined Seg X -defined NAT -valued {0} -valued Function-like constant total total V24( Seg X,{0}) Function-yielding V28() finite FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support Element of bool [:(Seg X),{0}:]
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
[:(Seg X),{0}:] is Relation-like finite countable set
bool [:(Seg X),{0}:] is non empty finite V40() countable set
(X -BinarySequence 0) . S is set
(X -BinarySequence 0) /. S is boolean Element of BOOLEAN
(X,(X -BinarySequence 0),F) . S is set
F /. S is boolean Element of BOOLEAN
FALSE '&' (F /. S) is boolean Element of BOOLEAN
K161(FALSE,(F /. S)) is set
X is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
X -BinarySequence 0 is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
'not' (X -BinarySequence 0) is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
F is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
(X,('not' (X -BinarySequence 0)),F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom (X -BinarySequence 0) is finite X -element countable Element of bool NAT
Seg X is finite X -element countable Element of bool NAT
dom (X,('not' (X -BinarySequence 0)),F) is finite X -element countable Element of bool NAT
dom F is finite X -element countable Element of bool NAT
S is set
0* X is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of REAL X
REAL X is functional FinSequence-membered FinSequenceSet of REAL
X |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like Function-yielding V28() finite X -element FinSequence-like FinSubsequence-like Cardinal-yielding countable FinSequence-yielding finite-support Element of X -tuples_on NAT
X -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of NAT * : len b1 = X } is set
(Seg X) --> 0 is Relation-like Seg X -defined Seg X -defined NAT -valued {0} -valued Function-like constant total total V24( Seg X,{0}) Function-yielding V28() finite FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support Element of bool [:(Seg X),{0}:]
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
[:(Seg X),{0}:] is Relation-like finite countable set
bool [:(Seg X),{0}:] is non empty finite V40() countable set
(X -BinarySequence 0) . S is set
(X -BinarySequence 0) /. S is boolean Element of BOOLEAN
('not' (X -BinarySequence 0)) /. S is boolean Element of BOOLEAN
ck is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(X -BinarySequence 0) /. ck is boolean Element of BOOLEAN
'not' ((X -BinarySequence 0) /. ck) is boolean Element of BOOLEAN
K164(1,((X -BinarySequence 0) /. ck)) is set
TRUE is boolean Element of BOOLEAN
(X,('not' (X -BinarySequence 0)),F) . S is set
F /. S is boolean Element of BOOLEAN
TRUE '&' (F /. S) is boolean Element of BOOLEAN
K161(TRUE,(F /. S)) is set
F . S is set
X is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
F is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
2 to_power F is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
X -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite X -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
F + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(X -BinarySequence (2 to_power F)) . (F + 1) is set
Seg X is finite X -element countable Element of bool NAT
TRUE is boolean Element of BOOLEAN
dcF is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dcF -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite dcF -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H1(dcF) . (F + 1) is set
dcF + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
0* dcF is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of REAL dcF
REAL dcF is functional FinSequence-membered FinSequenceSet of REAL
dcF |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like Function-yielding V28() finite dcF -element FinSequence-like FinSubsequence-like Cardinal-yielding countable FinSequence-yielding finite-support Element of dcF -tuples_on NAT
dcF -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of NAT * : len b1 = dcF } is set
Seg dcF is finite dcF -element countable Element of bool NAT
(Seg dcF) --> 0 is Relation-like Seg dcF -defined Seg dcF -defined NAT -valued {0} -valued Function-like constant total total V24( Seg dcF,{0}) Function-yielding V28() finite FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support Element of bool [:(Seg dcF),{0}:]
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
[:(Seg dcF),{0}:] is Relation-like finite countable set
bool [:(Seg dcF),{0}:] is non empty finite V40() countable set
dom (0* dcF) is finite countable Element of bool NAT
len (0* dcF) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
<*TRUE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
dom <*TRUE*> is non empty trivial finite 1 -element countable Element of bool NAT
(dcF + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite dcF + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H1(dcF + 1) . (F + 1) is set
(0* dcF) ^ <*TRUE*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
((0* dcF) ^ <*TRUE*>) . (F + 1) is set
<*TRUE*> . 1 is set
0* dcF is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of REAL dcF
REAL dcF is functional FinSequence-membered FinSequenceSet of REAL
dcF |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like Function-yielding V28() finite dcF -element FinSequence-like FinSubsequence-like Cardinal-yielding countable FinSequence-yielding finite-support Element of dcF -tuples_on NAT
dcF -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of NAT * : len b1 = dcF } is set
Seg dcF is finite dcF -element countable Element of bool NAT
(Seg dcF) --> 0 is Relation-like Seg dcF -defined Seg dcF -defined NAT -valued {0} -valued Function-like constant total total V24( Seg dcF,{0}) Function-yielding V28() finite FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support Element of bool [:(Seg dcF),{0}:]
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
[:(Seg dcF),{0}:] is Relation-like finite countable set
bool [:(Seg dcF),{0}:] is non empty finite V40() countable set
dom (0* dcF) is finite countable Element of bool NAT
len (0* dcF) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
<*TRUE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
dom <*TRUE*> is non empty trivial finite 1 -element countable Element of bool NAT
(dcF + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite dcF + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H1(dcF + 1) . (F + 1) is set
(0* dcF) ^ <*TRUE*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
((0* dcF) ^ <*TRUE*>) . (F + 1) is set
<*TRUE*> . 1 is set
0 + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
Seg dcF is finite dcF -element countable Element of bool NAT
dom H1(dcF) is finite dcF -element countable Element of bool NAT
2 to_power dcF is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(dcF + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite dcF + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H1(dcF + 1) . (F + 1) is set
S is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
<*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
H1(S) ^ <*FALSE*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element K288(S,1) -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
K288(S,1) is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(H1(S) ^ <*FALSE*>) . (F + 1) is set
(dcF + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite dcF + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H1(dcF + 1) . (F + 1) is set
(dcF + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite dcF + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H1(dcF + 1) . (F + 1) is set
0 -BinarySequence (2 to_power F) is empty proper ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined BOOLEAN -valued Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support FinSequence of BOOLEAN
[:NAT,BOOLEAN:] is non empty non trivial Relation-like non finite set
H1( 0 ) . (F + 1) is set
dcF is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(X -BinarySequence (2 to_power F)) . dcF is set
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
0 + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom H1(S + 1) is finite S + 1 -element countable Element of bool NAT
Seg (S + 1) is non empty finite S + 1 -element S + 1 -element countable Element of bool NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
H1(S + 1) . (S + 1) is set
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
dom H1(S + 1) is finite S + 1 -element countable Element of bool NAT
Seg (S + 1) is non empty finite S + 1 -element S + 1 -element countable Element of bool NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
H1(S + 1) . (S + 1) is set
2 to_power S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
H1(S + 1) . (S + 1) is set
dom H1(S + 1) is finite S + 1 -element countable Element of bool NAT
Seg (S + 1) is non empty finite S + 1 -element S + 1 -element countable Element of bool NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
dom H1(S) is finite S -element countable Element of bool NAT
Seg S is finite S -element countable Element of bool NAT
len H1(S) is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
<*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
dom <*FALSE*> is non empty trivial finite 1 -element countable Element of bool NAT
ck is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H1(ck) ^ <*FALSE*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like finite ck + 1 -element K288(ck,1) -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
K288(ck,1) is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(H1(ck) ^ <*FALSE*>) . (S + 1) is set
<*FALSE*> . 1 is set
Seg S is finite S -element countable Element of bool NAT
dom H1(S) is finite S -element countable Element of bool NAT
ck is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
<*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
H1(ck) ^ <*FALSE*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like finite ck + 1 -element K288(ck,1) -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
K288(ck,1) is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(H1(ck) ^ <*FALSE*>) . (S + 1) is set
H1(S) . (S + 1) is set
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
((S + 1) -BinarySequence (2 to_power F)) . (S + 1) is set
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(0 -BinarySequence (2 to_power F)) . (S + 1) is empty ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support set
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H1(S + 1) . S is set
dom H1(S) is finite S -element countable Element of bool NAT
Seg S is finite S -element countable Element of bool NAT
2 to_power S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H1(S + 1) . S is set
ck is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite ck -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
<*FALSE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
H1(ck) ^ <*FALSE*> is non empty Relation-like NAT -defined BOOLEAN -valued Function-like finite ck + 1 -element K288(ck,1) -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
K288(ck,1) is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
ck + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(H1(ck) ^ <*FALSE*>) . S is set
H1(S) . S is set
Seg S is finite S -element countable Element of bool NAT
0* S is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of REAL S
REAL S is functional FinSequence-membered FinSequenceSet of REAL
S |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like Function-yielding V28() finite S -element FinSequence-like FinSubsequence-like Cardinal-yielding countable FinSequence-yielding finite-support Element of S -tuples_on NAT
S -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like countable finite-support Element of NAT * : len b1 = S } is set
(Seg S) --> 0 is Relation-like Seg S -defined Seg S -defined NAT -valued {0} -valued Function-like constant total total V24( Seg S,{0}) Function-yielding V28() finite FinSequence-like FinSubsequence-like Cardinal-yielding countable finite-support Element of bool [:(Seg S),{0}:]
{0} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
[:(Seg S),{0}:] is Relation-like finite countable set
bool [:(Seg S),{0}:] is non empty finite V40() countable set
dom (0* S) is finite countable Element of bool NAT
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
H1(S + 1) . S is set
<*TRUE*> is non empty trivial Relation-like NAT -defined BOOLEAN -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable finite-support Element of BOOLEAN *
BOOLEAN * is non empty functional FinSequence-membered FinSequenceSet of BOOLEAN
(0* S) ^ <*TRUE*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable finite-support set
((0* S) ^ <*TRUE*>) . S is set
(0* S) . S is set
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
(S + 1) -BinarySequence (2 to_power F) is Relation-like NAT -defined BOOLEAN -valued Function-like finite S + 1 -element FinSequence-like FinSubsequence-like countable finite-support FinSequence of BOOLEAN
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
((S + 1) -BinarySequence (2 to_power F)) . S is set
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
(0 -BinarySequence (2 to_power F)) . S is empty ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional Function-yielding V28() V29() V30() V31() V33() V34() V35() finite finite-yielding V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V48() V49() Cardinal-yielding with_common_domain countable FinSequence-yielding finite-support set
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable set
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable set
S + 1 is non empty ext-real positive non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
2 to_power S is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable Element of NAT
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[{},{}] is V21() set
{{},{}} is non empty functional finite V40() countable set
{{}} is non empty trivial functional finite V40() 1 -element with_common_domain countable set
{{{},{}},{{}}} is non empty finite V40() countable set
{[{},{}]} is non empty trivial Relation-like Function-like constant finite 1 -element countable finite-support set
F is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
X is set
bool X is non empty set
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
(X) is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
K is Element of F
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is set
K is set
dcF is set
[K,dcF] is V21() set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
S is Element of bool X
S is Element of bool X
ck is Element of bool X
B is Element of bool X
[ck,B] is V21() set
{ck,B} is non empty finite countable set
{ck} is non empty trivial finite 1 -element countable set
{{ck,B},{ck}} is non empty finite V40() countable set
K is Element of bool X
dcF is Element of bool X
[K,dcF] is V21() set
{K,dcF} is non empty finite countable set
{K} is non empty trivial finite 1 -element countable set
{{K,dcF},{K}} is non empty finite V40() countable set
X is set
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
F is set
K is Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
dcF is set
S is set
[dcF,S] is V21() set
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
S is Element of bool X
ck is Element of bool X
[S,ck] is V21() set
{S,ck} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,ck},{S}} is non empty finite V40() countable set
X is ()
the of X is non empty finite countable set
bool the of X is non empty finite V40() countable set
X is ()
the of X is non empty finite countable set
bool the of X is non empty finite V40() countable set
X is ()
the of X is non empty finite countable set
bool the of X is non empty finite V40() countable set
{ [b1,b2] where b1, b2 is finite countable Element of bool the of X : (X,b1,b2) } is set
bool the of X is non empty finite V40() countable Element of bool (bool the of X)
bool (bool the of X) is non empty finite V40() countable set
[:(bool the of X),(bool the of X):] is non empty Relation-like finite countable set
bool [:(bool the of X),(bool the of X):] is non empty finite V40() countable set
[:(bool the of X),(bool the of X):] is non empty Relation-like bool the of X -defined bool the of X -valued finite countable Element of bool [:(bool the of X),(bool the of X):]
[:(bool the of X),(bool the of X):] is non empty Relation-like finite countable set
bool [:(bool the of X),(bool the of X):] is non empty finite V40() countable set
dcF is set
S is finite countable Element of bool the of X
S is finite countable Element of bool the of X
[S,S] is V21() set
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
X is ()
the of X is non empty finite countable set
bool the of X is non empty finite V40() countable set
(X) is Relation-like bool the of X -defined bool the of X -valued finite countable Element of bool [:(bool the of X),(bool the of X):]
bool the of X is non empty finite V40() countable Element of bool (bool the of X)
bool (bool the of X) is non empty finite V40() countable set
[:(bool the of X),(bool the of X):] is non empty Relation-like finite countable set
bool [:(bool the of X),(bool the of X):] is non empty finite V40() countable set
{ [b1,b2] where b1, b2 is finite countable Element of bool the of X : (X,b1,b2) } is set
F is finite countable Element of bool the of X
K is finite countable Element of bool the of X
[F,K] is V21() set
{F,K} is non empty finite V40() countable set
{F} is non empty trivial finite V40() 1 -element countable set
{{F,K},{F}} is non empty finite V40() countable set
S is finite countable Element of bool the of X
S is finite countable Element of bool the of X
[S,S] is V21() set
{S,S} is non empty finite V40() countable set
{S} is non empty trivial finite V40() 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
dcF is Element of (X)
dcF `1 is set
S is Element of (X)
S `2 is set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
K is Element of (X)
F is Element of (X)
K `1 is set
F `1 is set
F `2 is set
K `2 is set
[(F `1),(F `2)] is V21() set
{(F `1),(F `2)} is non empty finite countable set
{(F `1)} is non empty trivial finite 1 -element countable set
{{(F `1),(F `2)},{(F `1)}} is non empty finite V40() countable set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
K is Element of (X)
F is Element of (X)
dcF is Element of (X)
K `2 is set
dcF `2 is set
F `2 is set
dcF `1 is set
K `1 is set
F `1 is set
X is set
bool X is non empty set
F is Element of bool X
K is Element of bool X
[F,K] is V21() set
{F,K} is non empty finite countable set
{F} is non empty trivial finite 1 -element countable set
{{F,K},{F}} is non empty finite V40() countable set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
X is set
bool X is non empty set
F is Element of bool X
K is Element of bool X
(X,F,K) is V21() Element of (X)
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{F,K} is non empty finite countable set
{F} is non empty trivial finite 1 -element countable set
{{F,K},{F}} is non empty finite V40() countable set
dcF is Element of bool X
S is Element of bool X
(X,dcF,S) is V21() Element of (X)
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
(X,F,K) `2 is set
(X,dcF,S) `1 is set
(X,dcF,S) `2 is set
(X,F,K) `1 is set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
{ [b1,b2] where b1, b2 is Element of (X) : (X,b2,b1) } is set
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
[:(X),(X):] is non empty Relation-like [:(bool X),(bool X):] -defined [:(bool X),(bool X):] -valued Element of bool [:[:(bool X),(bool X):],[:(bool X),(bool X):]:]
[:[:(bool X),(bool X):],[:(bool X),(bool X):]:] is non empty Relation-like set
bool [:[:(bool X),(bool X):],[:(bool X),(bool X):]:] is non empty set
K is set
dcF is Element of (X)
S is Element of (X)
[dcF,S] is V21() set
{dcF,S} is non empty finite countable set
{dcF} is non empty trivial finite 1 -element countable set
{{dcF,S},{dcF}} is non empty finite V40() countable set
K is set
(K) is non empty Relation-like bool K -defined bool K -valued Element of bool [:(bool K),(bool K):]
bool K is non empty Element of bool (bool K)
bool K is non empty set
bool (bool K) is non empty set
[:(bool K),(bool K):] is non empty Relation-like set
bool [:(bool K),(bool K):] is non empty set
[:(bool K),(bool K):] is non empty Relation-like bool K -defined bool K -valued Element of bool [:(bool K),(bool K):]
[:(bool K),(bool K):] is non empty Relation-like set
bool [:(bool K),(bool K):] is non empty set
F is set
X is set
(X) is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty set
{ [b1,b2] where b1, b2 is Element of (X) : (X,b2,b1) } is set
dcF is set
S is Element of (K)
S is Element of (K)
[S,S] is V21() set
{S,S} is non empty finite countable set
{S} is non empty trivial finite 1 -element countable set
{{S,S},{S}} is non empty finite V40() countable set
(K) is Relation-like (K) -defined (K) -valued Element of bool [:(K),(K):]
[:(K),(K):] is non empty Relation-like set
bool [:(K),(K):] is non empty set
{ [b1,b2] where b1, b2 is Element of (K) : (K,b2,b1) } is set
X is set
(X) is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
[:(bool X),(bool X):] is non empty Relation-like bool X -defined bool X -valued Element of bool [:(bool X),(bool X):]
[:(bool X),(bool X):] is non empty Relation-like set
bool [:(bool X),(bool X):] is non empty set
(X) is Relation-like (X) -defined (X) -valued Element of bool [:(X),(X):]
[:(X),(X):] is non empty Relation-like set
bool [:(X),(X):] is non empty