:: ARMSTRNG semantic presentation

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

{ b

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

F

bool F

X is Element of bool F

F is Element of bool F

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

{ b

K is set

dcF is Element of X

K is Element of bool X

dcF is set

S is Element of X

F

{ b

X is set

{ b

F is set

K is Element of F

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 F

{ b

card H

K is ext-real non negative V29() V30() V31() V35() finite cardinal V48() V49() countable set

dcF is Element of F

{ b

card { b

dcF is Element of F

{ b

card H

S is set

S is Element of F

S is set

ck is set

S /\ ck is set

{ b

B is set

m is Element of F

{ b

m is set

P is Element of F

m is finite countable set

S is finite countable set

y9 is set

P is Element of F

a is Element of F

P is Element of F

y9 is Element of F

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 F

a is Element of F

x9 is Element of F

y9 is Element of F

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

{ b

[: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

{ b

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

{ b

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

{ b

(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

{ b

(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

H

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

{ b

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

H

(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

{ b

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

H

(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 H

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

H

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

H

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

(H

(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

H

(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

H

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

H

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 H

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

H

(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 H

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

H

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

H

dom H

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 H

Seg S is finite S -element countable Element of bool NAT

len H

<*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

H

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

(H

<*FALSE*> . 1 is set

Seg S is finite S -element countable Element of bool NAT

dom H

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

H

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

(H

H

(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

H

dom H

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

H

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

H

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

(H

H

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

{ b

(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

H

<*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

{ [b

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

{ [b

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

{ [b

[:(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

{ [b

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

{ [b

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