:: FOMODEL4 semantic presentation

REAL is non empty non trivial non finite non empty-membered set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal non empty-membered countable denumerable Element of bool REAL
bool REAL is non empty non trivial non finite non empty-membered set
BOOLEAN is non empty set
NAT is non empty non trivial V4() V5() V6() non finite cardinal limit_cardinal non empty-membered countable denumerable set
bool NAT is non empty non trivial non finite non empty-membered set
bool NAT is non empty non trivial non finite non empty-membered set
COMPLEX is non empty non trivial non finite non empty-membered set
RAT is non empty non trivial non finite non empty-membered set
INT is non empty non trivial non finite non empty-membered set
{} is empty trivial V4() V5() V6() V8() V9() V10() complex ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V156() FuncSeq-like empty-membered Cardinal-yielding with_common_domain countable V208() V209() set
{{}} is non empty trivial functional finite V36() 1 -element empty-membered with_common_domain countable set
1 is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable Element of NAT
{} * is non empty functional V36() FinSequence-membered FinSequenceSet of {}
[:{{}},NAT:] is non empty non trivial Relation-like non finite non empty-membered set
[{},{}] is non empty V26() set
{[{},{}]} is non empty trivial Relation-like Function-like constant finite 1 -element with_non-empty_elements non empty-membered countable V209() set
[:{{}},NAT:] \ {[{},{}]} is non empty non trivial Relation-like {{}} -defined NAT -valued non finite non empty-membered Element of bool [:{{}},NAT:]
bool [:{{}},NAT:] is non empty non trivial non finite non empty-membered set
[:{{}},NAT:] typed\ {[{},{}]} is Relation-like {{}} -defined NAT -valued Element of bool [:{{}},NAT:]
NAT \/ ([:{{}},NAT:] \ {[{},{}]}) is non empty non trivial non finite non empty-membered set
[:REAL,REAL:] is non empty non trivial Relation-like non finite non empty-membered set
bool [:REAL,REAL:] is non empty non trivial non finite non empty-membered set
K281() is V47() V75() L8()
the U1 of K281() is set
K286() is V47() L8()
K287() is V47() V75() M13(K286())
K288() is V47() V75() V97() V154() M16(K286(),K287())
K290() is V47() V75() V97() V99() V101() L8()
K291() is V47() V75() V97() V154() M13(K290())
2 is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable Element of NAT
{{},1} is non empty finite V36() countable set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite non empty-membered set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite non empty-membered set
0 is empty trivial V4() V5() V6() V8() V9() V10() complex ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V156() FuncSeq-like empty-membered Cardinal-yielding with_common_domain countable V208() V209() Element of NAT
id BOOLEAN is non empty Relation-like BOOLEAN -defined BOOLEAN -valued Function-like one-to-one total quasi_total onto bijective reflexive symmetric antisymmetric transitive boolean-valued Element of bool [:BOOLEAN,BOOLEAN:]
[:BOOLEAN,BOOLEAN:] is non empty Relation-like set
bool [:BOOLEAN,BOOLEAN:] is non empty set
3 is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable Element of NAT
proj1 {} is empty trivial V4() V5() V6() V8() V9() V10() complex ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined NAT -defined {{}} -valued {{}} -valued Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element {} -element V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V156() FuncSeq-like empty-membered Cardinal-yielding with_common_domain countable V208() V209() set
proj2 {} is empty trivial V4() V5() V6() V8() V9() V10() complex ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined NAT -defined {{}} -valued {{}} -valued Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element {} -element V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V156() FuncSeq-like with_non-empty_elements empty-membered Cardinal-yielding with_common_domain countable V208() V209() set
len {} is empty trivial V4() V5() V6() V8() V9() V10() complex ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined {{}} -valued Function-like one-to-one constant functional finite finite-yielding V36() cardinal {} -element V40() V41() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V156() FuncSeq-like empty-membered Cardinal-yielding with_common_domain countable V208() V209() Element of NAT
Seg 1 is non empty trivial finite 1 -element countable Element of bool NAT
{ b₁ where b₁ is V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty trivial finite V36() 1 -element with_non-empty_elements non empty-membered countable Element of bool NAT
- 2 is non empty complex ext-real non positive negative finite V40() V41() countable set
TRUE is boolean Element of BOOLEAN
FALSE is boolean Element of BOOLEAN
X is set
C is set
phi is set
Funcs (C,phi) is functional set
bool (Funcs (C,phi)) is non empty set
[:C,phi:] is Relation-like set
bool [:C,phi:] is non empty set
bool (bool [:C,phi:]) is non empty set
bool [:C,phi:] is non empty Element of bool (bool [:C,phi:])
X is V51() V53() eligible Language-like
TermSymbolsOf X is non empty set
the U1 of X is set
the U3 of X is Element of the U1 of X
{ the U3 of X} is non empty trivial finite 1 -element countable set
the U1 of X \ { the U3 of X} is non empty Element of bool the U1 of X
bool the U1 of X is non empty set
the U1 of X typed\ { the U3 of X} is Element of bool the U1 of X
the adicity of X is non empty Relation-like the U1 of X \ { the U3 of X} -defined INT -valued Function-like total quasi_total Element of bool [:( the U1 of X \ { the U3 of X}),INT:]
[:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial Relation-like non finite non empty-membered set
bool [:( the U1 of X \ { the U3 of X}),INT:] is non empty non trivial non finite non empty-membered set
the adicity of X " NAT is Element of bool ( the U1 of X \ { the U3 of X})
bool ( the U1 of X \ { the U3 of X}) is non empty set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
TheEqSymbOf X is low-compounding relational non own ofAtomicFormula Element of AllSymbolsOf X
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U2 of X is Element of the U1 of X
<*(TheEqSymbOf X)*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}}
[1,(TheEqSymbOf X)] is non empty V26() set
{[1,(TheEqSymbOf X)]} is non empty trivial Relation-like Function-like constant finite 1 -element with_non-empty_elements non empty-membered countable V209() set
AtomicFormulaSymbolsOf X is non empty Element of bool (AllSymbolsOf X)
bool (AllSymbolsOf X) is non empty non trivial non finite non empty-membered set
TheNorSymbOf X is set
{(TheNorSymbOf X)} is non empty trivial finite 1 -element countable set
(AllSymbolsOf X) \ {(TheNorSymbOf X)} is non empty non trivial non finite non empty-membered Element of bool (AllSymbolsOf X)
bool (AllSymbolsOf X) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) typed\ {(TheNorSymbOf X)} is Element of bool (AllSymbolsOf X)
C is non empty Relation-like NAT -defined TermSymbolsOf X -valued Function-like finite FinSequence-like FinSubsequence-like countable V209() termal Element of ((AllSymbolsOf X) *) \ {{}}
<*(TheEqSymbOf X)*> ^ C is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}}
phi is non empty Relation-like NAT -defined TermSymbolsOf X -valued Function-like finite FinSequence-like FinSubsequence-like countable V209() termal Element of ((AllSymbolsOf X) *) \ {{}}
(<*(TheEqSymbOf X)*> ^ C) ^ phi is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}}
AllTermsOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered Element of bool (bool (((AllSymbolsOf X) *) \ {{}}))
bool (bool (((AllSymbolsOf X) *) \ {{}})) is non empty non trivial non finite non empty-membered set
X -termsOfMaxDepth is Relation-like Function-like set
proj2 (X -termsOfMaxDepth) is set
union (proj2 (X -termsOfMaxDepth)) is set
X -multiCat is non empty Relation-like ((AllSymbolsOf X) *) * -defined (AllSymbolsOf X) * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:(((AllSymbolsOf X) *) *),((AllSymbolsOf X) *):]
((AllSymbolsOf X) *) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (AllSymbolsOf X) *
[:(((AllSymbolsOf X) *) *),((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:(((AllSymbolsOf X) *) *),((AllSymbolsOf X) *):] is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) -multiCat is non empty Relation-like ((AllSymbolsOf X) *) * -defined (AllSymbolsOf X) * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:(((AllSymbolsOf X) *) *),((AllSymbolsOf X) *):]
{} .--> {} is non empty trivial Relation-like {{}} -defined Function-like one-to-one constant finite 1 -element Function-yielding V156() Cardinal-yielding countable V209() set
{{}} --> {} is non empty Relation-like empty-yielding {{}} -defined INT -valued {{}} -valued Function-like constant total quasi_total finite Function-yielding V156() Cardinal-yielding countable V209() Element of bool [:{{}},{{}}:]
[:{{}},{{}}:] is non empty Relation-like finite countable set
bool [:{{}},{{}}:] is non empty finite V36() countable set
K295((AllSymbolsOf X)) is non empty Relation-like [:((AllSymbolsOf X) *),((AllSymbolsOf X) *):] -defined (AllSymbolsOf X) * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:[:((AllSymbolsOf X) *),((AllSymbolsOf X) *):],((AllSymbolsOf X) *):]
[:((AllSymbolsOf X) *),((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite non empty-membered set
[:[:((AllSymbolsOf X) *),((AllSymbolsOf X) *):],((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:[:((AllSymbolsOf X) *),((AllSymbolsOf X) *):],((AllSymbolsOf X) *):] is non empty non trivial non finite non empty-membered set
MultPlace K295((AllSymbolsOf X)) is non empty Relation-like (((AllSymbolsOf X) *) *) \ {{}} -defined (AllSymbolsOf X) * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:((((AllSymbolsOf X) *) *) \ {{}}),((AllSymbolsOf X) *):]
(((AllSymbolsOf X) *) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (((AllSymbolsOf X) *) *)
bool (((AllSymbolsOf X) *) *) is non empty non trivial non finite non empty-membered set
(((AllSymbolsOf X) *) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool (((AllSymbolsOf X) *) *)
[:((((AllSymbolsOf X) *) *) \ {{}}),((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:((((AllSymbolsOf X) *) *) \ {{}}),((AllSymbolsOf X) *):] is non empty non trivial non finite non empty-membered set
({} .--> {}) +* (MultPlace K295((AllSymbolsOf X))) is non empty Relation-like Function-like Function-yielding V156() set
(((AllSymbolsOf X) *) \ {{}}) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of ((AllSymbolsOf X) *) \ {{}}
(AllTermsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered Element of bool ((((AllSymbolsOf X) *) \ {{}}) *)
bool ((((AllSymbolsOf X) *) \ {{}}) *) is non empty non trivial non finite non empty-membered set
Y is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() termal Element of AllTermsOf X
<*Y*> is non empty trivial Relation-like non empty-yielding NAT -defined AllTermsOf X -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Function-yielding V156() FuncSeq-like countable V208() V209() FinSequence of AllTermsOf X
[1,Y] is non empty V26() set
{[1,Y]} is non empty trivial Relation-like Function-like constant finite 1 -element with_non-empty_elements non empty-membered countable V209() set
phii is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() termal Element of AllTermsOf X
<*phii*> is non empty trivial Relation-like non empty-yielding NAT -defined AllTermsOf X -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Function-yielding V156() FuncSeq-like countable V208() V209() FinSequence of AllTermsOf X
[1,phii] is non empty V26() set
{[1,phii]} is non empty trivial Relation-like Function-like constant finite 1 -element with_non-empty_elements non empty-membered countable V209() set
<*Y*> ^ <*phii*> is non empty Relation-like non empty-yielding NAT -defined AllTermsOf X -valued Function-like finite 1 + 1 -element 1 + 1 -element FinSequence-like FinSubsequence-like Function-yielding V156() countable V208() V209() FinSequence of AllTermsOf X
1 + 1 is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable set
1 + 1 is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable Element of NAT
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
H is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
((AllSymbolsOf X) *) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of (AllSymbolsOf X) *
H * is non empty functional V36() FinSequence-membered Element of bool (((AllSymbolsOf X) *) *)
bool (((AllSymbolsOf X) *) *) is non empty non trivial non finite non empty-membered set
psi is Relation-like NAT -defined AllTermsOf X -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like Function-yielding V156() countable V208() V209() Element of (AllTermsOf X) *
m is Relation-like NAT -defined H -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V156() countable V209() Element of H *
abs (- 2) is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable Element of NAT
- (- 2) is non empty V4() V5() V6() V10() complex ext-real positive non negative finite cardinal V40() V41() countable set
HH is ofAtomicFormula Element of AllSymbolsOf X
ar HH is complex ext-real finite V40() V41() countable Element of INT
the adicity of X . HH is set
abs (ar HH) is V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable Element of NAT
(X -multiCat) . m is Relation-like NAT -defined AllSymbolsOf X -valued Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of (AllSymbolsOf X) *
(X -multiCat) . psi is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() set
a is non empty set
D2 is Element of a
<*D2*> is non empty trivial Relation-like NAT -defined a -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like countable V209() FinSequence of a
[1,D2] is non empty V26() set
{[1,D2]} is non empty trivial Relation-like Function-like constant finite 1 -element with_non-empty_elements non empty-membered countable V209() set
sub1 is Relation-like NAT -defined AllSymbolsOf X -valued Function-like finite FinSequence-like FinSubsequence-like countable V209() FinSequence of AllSymbolsOf X
HC is Relation-like NAT -defined AllSymbolsOf X -valued Function-like finite FinSequence-like FinSubsequence-like countable V209() FinSequence of AllSymbolsOf X
sub1 ^ HC is Relation-like NAT -defined AllSymbolsOf X -valued Function-like finite FinSequence-like FinSubsequence-like countable V209() FinSequence of AllSymbolsOf X
sub2 is non empty Relation-like NAT -defined AllSymbolsOf X -valued Function-like finite FinSequence-like FinSubsequence-like countable V209() FinSequence of AllSymbolsOf X
(AllSymbolsOf X) -multiCat is non empty Relation-like ((AllSymbolsOf X) *) * -defined (AllSymbolsOf X) * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:(((AllSymbolsOf X) *) *),((AllSymbolsOf X) *):]
[:(((AllSymbolsOf X) *) *),((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:(((AllSymbolsOf X) *) *),((AllSymbolsOf X) *):] is non empty non trivial non finite non empty-membered set
K295((AllSymbolsOf X)) is non empty Relation-like [:((AllSymbolsOf X) *),((AllSymbolsOf X) *):] -defined (AllSymbolsOf X) * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:[:((AllSymbolsOf X) *),((AllSymbolsOf X) *):],((AllSymbolsOf X) *):]
[:((AllSymbolsOf X) *),((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite non empty-membered set
[:[:((AllSymbolsOf X) *),((AllSymbolsOf X) *):],((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:[:((AllSymbolsOf X) *),((AllSymbolsOf X) *):],((AllSymbolsOf X) *):] is non empty non trivial non finite non empty-membered set
MultPlace K295((AllSymbolsOf X)) is non empty Relation-like (((AllSymbolsOf X) *) *) \ {{}} -defined (AllSymbolsOf X) * -valued Function-like total quasi_total Function-yielding V156() V208() Element of bool [:((((AllSymbolsOf X) *) *) \ {{}}),((AllSymbolsOf X) *):]
(((AllSymbolsOf X) *) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool (((AllSymbolsOf X) *) *)
(((AllSymbolsOf X) *) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool (((AllSymbolsOf X) *) *)
[:((((AllSymbolsOf X) *) *) \ {{}}),((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:((((AllSymbolsOf X) *) *) \ {{}}),((AllSymbolsOf X) *):] is non empty non trivial non finite non empty-membered set
({} .--> {}) +* (MultPlace K295((AllSymbolsOf X))) is non empty Relation-like Function-like Function-yielding V156() set
<*Y,phii*> is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like Function-yielding V156() countable V209() set
<*Y*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Function-yielding V156() FuncSeq-like countable V208() V209() set
<*phii*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Function-yielding V156() FuncSeq-like countable V208() V209() set
<*Y*> ^ <*phii*> is non empty Relation-like NAT -defined Function-like finite 1 + 1 -element 1 + 1 -element FinSequence-like FinSubsequence-like Function-yielding V156() countable V208() V209() set
((AllSymbolsOf X) -multiCat) . <*Y,phii*> is Relation-like NAT -defined AllSymbolsOf X -valued Function-like finite FinSequence-like FinSubsequence-like countable V209() set
Y ^ phii is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}}
C ^ phi is non empty Relation-like NAT -defined TermSymbolsOf X -valued Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}}
<*(TheEqSymbOf X)*> ^ (C ^ phi) is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}}
X is V51() V53() eligible Language-like
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } is set
X is V51() V53() eligible Language-like
(X) is set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } is set
the functional finite V36() FinSequence-membered with_non-empty_elements countable Element of bool (AllFormulasOf X) is functional finite V36() FinSequence-membered with_non-empty_elements countable Element of bool (AllFormulasOf X)
the non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}}
[ the functional finite V36() FinSequence-membered with_non-empty_elements countable Element of bool (AllFormulasOf X), the non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}}] is non empty V26() Element of [:(bool (AllFormulasOf X)),(((AllSymbolsOf X) *) \ {{}}):]
[:(bool (AllFormulasOf X)),(((AllSymbolsOf X) *) \ {{}}):] is non empty non trivial Relation-like non finite non empty-membered set
X is V51() V53() eligible Language-like
(X) is non empty set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } is set
DD is set
FF is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X)
D is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}}
[FF,D] is non empty V26() Element of [:(bool (AllFormulasOf X)),(((AllSymbolsOf X) *) \ {{}}):]
[:(bool (AllFormulasOf X)),(((AllSymbolsOf X) *) \ {{}}):] is non empty non trivial Relation-like non finite non empty-membered set
bool (AllFormulasOf X) is non empty Element of bool (bool (AllFormulasOf X))
bool (bool (AllFormulasOf X)) is non empty set
[:(bool (AllFormulasOf X)),(((AllSymbolsOf X) *) \ {{}}):] is non empty non trivial Relation-like bool (AllFormulasOf X) -defined (AllSymbolsOf X) * -valued non finite non empty-membered Element of bool [:(bool (AllFormulasOf X)),((AllSymbolsOf X) *):]
[:(bool (AllFormulasOf X)),((AllSymbolsOf X) *):] is non empty non trivial Relation-like non finite non empty-membered set
bool [:(bool (AllFormulasOf X)),((AllSymbolsOf X) *):] is non empty non trivial non finite non empty-membered set
bool [:(bool (AllFormulasOf X)),(((AllSymbolsOf X) *) \ {{}}):] is non empty non trivial non finite non empty-membered set
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } is set
bool (X) is non empty set
C is Relation-like Element of bool (X)
C is Element of (X)
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } is set
the (X) Element of (X) is (X) Element of (X)
bool (X) is non empty set
the Relation-like (X) Element of bool (X) is Relation-like (X) Element of bool (X)
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } is set
the (X) Element of (X) is (X) Element of (X)
(X) is non empty Relation-like set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } is set
bool (X) is non empty set
the Relation-like (X) Element of bool (X) is Relation-like (X) Element of bool (X)
X is set
C is set
Funcs (X,C) is functional set
bool (Funcs (X,C)) is non empty set
phi is functional Element of bool (Funcs (X,C))
union phi is Relation-like set
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } 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
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
bool (Funcs ((bool (X)),(bool (X)))) is non empty set
C is functional Element of bool (Funcs ((bool (X)),(bool (X))))
union C is Relation-like set
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } 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
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
bool (Funcs ((bool (X)),(bool (X)))) is non empty set
C is functional Element of bool (Funcs ((bool (X)),(bool (X))))
union C is Relation-like set
[:(bool (X)),(bool (X)):] is non empty Relation-like set
bool [:(bool (X)),(bool (X)):] is non empty set
DD is Relation-like bool (X) -defined bool (X) -valued Element of bool [:(bool (X)),(bool (X)):]
FF is non empty Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of bool [:(bool (X)),(bool (X)):]
D is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
Y is Relation-like (X) Element of bool (X)
D . Y is Relation-like (X) Element of bool (X)
{Y} is non empty trivial finite 1 -element countable Element of bool (bool (X))
bool (bool (X)) is non empty set
(union C) .: {Y} is set
union ((union C) .: {Y}) is set
DD is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
FF is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
[:(bool (X)),(bool (X)):] is non empty Relation-like set
bool [:(bool (X)),(bool (X)):] is non empty set
D is non empty Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of bool [:(bool (X)),(bool (X)):]
phii is Relation-like (X) Element of bool (X)
D . phii is Relation-like (X) Element of bool (X)
{phii} is non empty trivial finite 1 -element countable set
(union C) .: {phii} is set
union ((union C) .: {phii}) is set
Y is non empty Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of bool [:(bool (X)),(bool (X)):]
Y . phii is Relation-like (X) Element of bool (X)
X is V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set
C is V51() V53() eligible Language-like
(C) is non empty Relation-like set
AllFormulasOf C is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf C -prefix C -prefix Element of bool (((AllSymbolsOf C) *) \ {{}})
AllSymbolsOf C is non empty non trivial non finite non empty-membered set
the U1 of C is set
AllSymbolsOf C is non empty non trivial non finite non empty-membered set
(AllSymbolsOf C) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf C
((AllSymbolsOf C) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf C) *)
bool ((AllSymbolsOf C) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf C) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf C) *)
bool (((AllSymbolsOf C) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf C) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf C
((AllSymbolsOf C) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf C) *)
bool ((AllSymbolsOf C) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf C) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf C) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf C) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf C) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf C), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf C) *) \ {{}} : b₁ is finite } is set
bool (C) is non empty Element of bool (bool (C))
bool (C) is non empty set
bool (bool (C)) is non empty set
Funcs ((bool (C)),(bool (C))) is non empty functional FUNCTION_DOMAIN of bool (C), bool (C)
bool (Funcs ((bool (C)),(bool (C)))) is non empty set
[:(bool (C)),(bool (C)):] is non empty Relation-like set
bool [:(bool (C)),(bool (C)):] is non empty set
phi is functional Element of bool (Funcs ((bool (C)),(bool (C))))
(C,phi) is Relation-like bool (C) -defined bool (C) -valued Function-like total quasi_total Element of Funcs ((bool (C)),(bool (C)))
dom (C,phi) is Element of bool (bool (C))
bool (bool (C)) is non empty set
proj2 (C,phi) is set
iter ((C,phi),X) is Relation-like Function-like set
proj1 (iter ((C,phi),X)) is set
(dom (C,phi)) \/ (proj2 (C,phi)) is set
S is Relation-like bool (C) -defined bool (C) -valued Function-like total quasi_total Element of Funcs ((bool (C)),(bool (C)))
dom S is Element of bool (bool (C))
iter (S,X) is Relation-like Function-like set
proj1 (iter (S,X)) is set
DD is Relation-like (C) Element of bool (C)
FF is (C) set
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } 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
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
bool (Funcs ((bool (X)),(bool (X)))) is non empty set
C is functional Element of bool (Funcs ((bool (X)),(bool (X))))
(X,C) is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
phi is V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set
iter ((X,C),phi) is Relation-like Function-like set
[:(bool (X)),(bool (X)):] is non empty Relation-like set
bool [:(bool (X)),(bool (X)):] is non empty set
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } 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
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
bool (Funcs ((bool (X)),(bool (X)))) is non empty set
C is V51() V53() eligible Language-like
(C) is non empty Relation-like set
AllFormulasOf C is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf C -prefix C -prefix Element of bool (((AllSymbolsOf C) *) \ {{}})
AllSymbolsOf C is non empty non trivial non finite non empty-membered set
the U1 of C is set
AllSymbolsOf C is non empty non trivial non finite non empty-membered set
(AllSymbolsOf C) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf C
((AllSymbolsOf C) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf C) *)
bool ((AllSymbolsOf C) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf C) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf C) *)
bool (((AllSymbolsOf C) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf C) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf C
((AllSymbolsOf C) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf C) *)
bool ((AllSymbolsOf C) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf C) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf C) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf C) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf C) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf C), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf C) *) \ {{}} : b₁ is finite } is set
bool (C) is non empty Element of bool (bool (C))
bool (C) is non empty set
bool (bool (C)) is non empty set
Funcs ((bool (C)),(bool (C))) is non empty functional FUNCTION_DOMAIN of bool (C), bool (C)
bool (Funcs ((bool (C)),(bool (C)))) is non empty set
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } 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
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
bool (Funcs ((bool (X)),(bool (X)))) is non empty set
C is functional Element of bool (Funcs ((bool (X)),(bool (X))))
(X,C) is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
{ (iter ((X,C),b₁)) where b₁ is V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable Element of NAT : verum } is 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 [:(bool (X)),(bool (X)):] is non empty set
bool (bool [:(bool (X)),(bool (X)):]) is non empty set
FF is set
D is V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable Element of NAT
iter ((X,C),D) is Relation-like Function-like set
[:(bool (X)),(bool (X)):] is non empty Relation-like set
bool [:(bool (X)),(bool (X)):] is non empty set
bool [:(bool (X)),(bool (X)):] is non empty Element of bool (bool [:(bool (X)),(bool (X)):])
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } 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
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5() V6() V10() complex ext-real non negative finite cardinal V40() V41() countable set st b₁ is b₂ -wff } is set
bool (AllFormulasOf X) is non empty set
{ [b₁,b₂] where b₁ is functional V36() FinSequence-membered with_non-empty_elements Element of bool (AllFormulasOf X), b₂ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() wff Element of ((AllSymbolsOf X) *) \ {{}} : b₁ is finite } 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
Funcs ((bool (X)),(bool (X))) is non empty functional FUNCTION_DOMAIN of bool (X), bool (X)
id (bool (X)) is non empty Relation-like bool (X) -defined bool (X) -valued Function-like one-to-one total quasi_total onto bijective reflexive symmetric antisymmetric transitive 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
C is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
S is Relation-like bool (X) -defined bool (X) -valued Function-like total quasi_total Element of Funcs ((bool (X)),(bool (X)))
DD is Relation-like (X) Element of bool (X)
S . DD is Relation-like (X) Element of bool (X)
FF is Relation-like (X) Element of bool (X)
S . FF is Relation-like (X) Element of bool (X)
X is V51() V53() eligible Language-like
(X) is non empty Relation-like set
AllFormulasOf X is non empty functional V36() FinSequence-membered with_non-empty_elements non empty-membered AllSymbolsOf X -prefix X -prefix Element of bool (((AllSymbolsOf X) *) \ {{}})
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
the U1 of X is set
AllSymbolsOf X is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
bool (((AllSymbolsOf X) *) \ {{}}) is non empty non trivial non finite non empty-membered set
(AllSymbolsOf X) * is non empty non trivial functional non finite V36() FinSequence-membered non empty-membered FinSequenceSet of AllSymbolsOf X
((AllSymbolsOf X) *) \ {{}} is non empty non trivial functional non finite V36() FinSequence-membered with_non-empty_elements non empty-membered Element of bool ((AllSymbolsOf X) *)
bool ((AllSymbolsOf X) *) is non empty non trivial non finite non empty-membered set
((AllSymbolsOf X) *) typed\ {{}} is functional V36() FinSequence-membered Element of bool ((AllSymbolsOf X) *)
{ b₁ where b₁ is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like countable V209() Element of ((AllSymbolsOf X) *) \ {{}} : ex b₂ being V4() V5()