REAL is V56() V57() V58() V62() V74() V75() V77() set
NAT is non empty non trivial V35() V36() V37() V56() V57() V58() V59() V60() V61() V62() non finite V72() V74() V78() V79() Element of bool REAL
bool REAL is non empty cup-closed diff-closed preBoolean set
RAT is V56() V57() V58() V59() V62() set
{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V35() V36() V37() V39() V40() V41() V43() V44() V45() V46() V56() V57() V58() V59() V60() V61() V62() finite finite-yielding V67() V74() V75() V76() V77() V78() V80( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V93() set
the empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V35() V36() V37() V39() V40() V41() V43() V44() V45() V46() V56() V57() V58() V59() V60() V61() V62() finite finite-yielding V67() V74() V75() V76() V77() V78() V80( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V93() set is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V35() V36() V37() V39() V40() V41() V43() V44() V45() V46() V56() V57() V58() V59() V60() V61() V62() finite finite-yielding V67() V74() V75() V76() V77() V78() V80( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V93() set
COMPLEX is V56() V62() set
INT is V56() V57() V58() V59() V60() V62() set
NAT is non empty non trivial V35() V36() V37() V56() V57() V58() V59() V60() V61() V62() non finite V72() V74() V78() V79() set
bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set
bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set
[:COMPLEX,COMPLEX:] is Relation-like V43() set
bool [:COMPLEX,COMPLEX:] is non empty cup-closed diff-closed preBoolean set
[:COMPLEX,REAL:] is Relation-like V43() V44() V45() set
bool [:COMPLEX,REAL:] is non empty cup-closed diff-closed preBoolean set
1 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
2 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
3 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
A is non empty Relation-like QC-alphabet
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty cup-closed diff-closed preBoolean set
QC-symbols A is non empty set
p is Element of bound_QC-variables A
q is Element of QC-symbols A
x. q is Element of bound_QC-variables A
4 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
[4,q] is V18() set
{4,q} is non empty finite set
{4} is non empty trivial V56() V57() V58() V59() V60() V61() finite V67() V72() V73() V74() V75() V76() V80(1) set
{{4,q},{4}} is non empty finite V67() set
r is Element of QC-symbols A
x. r is Element of bound_QC-variables A
[4,r] is V18() set
{4,r} is non empty finite set
{{4,r},{4}} is non empty finite V67() set
A is set
p is set
A .--> p is Relation-like {A} -defined Function-like one-to-one finite set
{A} is non empty trivial finite V80(1) set
{A} --> p is non empty Relation-like {A} -defined {p} -valued Function-like constant total quasi_total finite Element of bool [:{A},{p}:]
{p} is non empty trivial finite V80(1) set
[:{A},{p}:] is non empty Relation-like finite set
bool [:{A},{p}:] is non empty cup-closed diff-closed preBoolean finite V67() set
q is Relation-like Function-like set
q +* (A .--> p) is Relation-like Function-like set
Im ((q +* (A .--> p)),A) is set
(q +* (A .--> p)) .: {A} is finite set
r is set
proj1 (q +* (A .--> p)) is set
f is set
(q +* (A .--> p)) . f is set
proj1 (A .--> p) is finite set
(A .--> p) . f is set
proj1 (A .--> p) is finite set
proj1 (q +* (A .--> p)) is set
(A .--> p) . A is set
(q +* (A .--> p)) . A is set
p is set
A is set
r is set
p --> r is Relation-like p -defined {r} -valued Function-like constant total quasi_total Element of bool [:p,{r}:]
{r} is non empty trivial finite V80(1) set
[:p,{r}:] is Relation-like set
bool [:p,{r}:] is non empty cup-closed diff-closed preBoolean set
f is Relation-like Function-like set
f +* (p --> r) is Relation-like Function-like set
(f +* (p --> r)) .: A is set
f .: A is set
(f .: A) \/ {r} is non empty set
h is set
proj1 (f +* (p --> r)) is set
u is set
(f +* (p --> r)) . u is set
proj1 (p --> r) is set
(p --> r) . u is set
f . u is set
proj1 f is set
A is set
p is set
A .--> p is Relation-like {A} -defined Function-like one-to-one finite set
{A} is non empty trivial finite V80(1) set
{A} --> p is non empty Relation-like {A} -defined {p} -valued Function-like constant total quasi_total finite Element of bool [:{A},{p}:]
{p} is non empty trivial finite V80(1) set
[:{A},{p}:] is non empty Relation-like finite set
bool [:{A},{p}:] is non empty cup-closed diff-closed preBoolean finite V67() set
q is Relation-like Function-like set
q +* (A .--> p) is Relation-like Function-like set
r is set
r \ {A} is Element of bool r
bool r is non empty cup-closed diff-closed preBoolean set
(q +* (A .--> p)) .: (r \ {A}) is set
q .: (r \ {A}) is set
f is set
proj1 (A .--> p) is finite set
proj1 (q +* (A .--> p)) is set
h is set
(q +* (A .--> p)) . h is set
proj1 q is set
q . h is set
f is set
proj1 q is set
h is set
q . h is set
proj1 (A .--> p) is finite set
(q +* (A .--> p)) . h is set
proj1 (q +* (A .--> p)) is set
p is set
A is set
{A} is non empty trivial finite V80(1) set
A .--> p is Relation-like {A} -defined Function-like one-to-one finite set
{A} --> p is non empty Relation-like {A} -defined {p} -valued Function-like constant total quasi_total finite Element of bool [:{A},{p}:]
{p} is non empty trivial finite V80(1) set
[:{A},{p}:] is non empty Relation-like finite set
bool [:{A},{p}:] is non empty cup-closed diff-closed preBoolean finite V67() set
q is Relation-like Function-like set
q +* (A .--> p) is Relation-like Function-like set
r is set
r \ {A} is Element of bool r
bool r is non empty cup-closed diff-closed preBoolean set
q .: (r \ {A}) is set
(q +* (A .--> p)) .: (r \ {A}) is set
(q +* (A .--> p)) .: r is set
((q +* (A .--> p)) .: r) \ {p} is Element of bool ((q +* (A .--> p)) .: r)
bool ((q +* (A .--> p)) .: r) is non empty cup-closed diff-closed preBoolean set
f is set
proj1 (A .--> p) is finite set
proj1 (q +* (A .--> p)) is set
h is set
(q +* (A .--> p)) . h is set
proj1 q is set
q . h is set
f is set
proj1 (q +* (A .--> p)) is set
h is set
(q +* (A .--> p)) . h is set
proj1 (A .--> p) is finite set
(A .--> p) . h is set
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is non empty cup-closed diff-closed preBoolean set
QC-pred_symbols A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is non empty cup-closed diff-closed preBoolean set
p is Element of CQC-WFF A
q is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q -ary_QC-pred_symbols A is non empty Element of bool (QC-pred_symbols A)
bool (QC-pred_symbols A) is non empty cup-closed diff-closed preBoolean set
r is Element of q -ary_QC-pred_symbols A
f is Relation-like NAT -defined QC-variables A -valued Function-like finite V80(q) FinSequence-like FinSubsequence-like FinSequence of QC-variables A
r ! f is Element of QC-WFF A
len f is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
fixed_QC-variables A is non empty Element of bool (QC-variables A)
{ (f . b1) where b1 is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT : ( 1 <= b1 & b1 <= len f & f . b1 in fixed_QC-variables A ) } is set
free_QC-variables A is non empty Element of bool (QC-variables A)
{ (f . b1) where b1 is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT : ( 1 <= b1 & b1 <= len f & f . b1 in free_QC-variables A ) } is set
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is non empty cup-closed diff-closed preBoolean set
p is Element of CQC-WFF A
q is Element of QC-WFF A
'not' q is Element of QC-WFF A
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is non empty cup-closed diff-closed preBoolean set
p is Element of CQC-WFF A
q is Element of QC-WFF A
r is Element of QC-WFF A
q '&' r is Element of QC-WFF A
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is non empty cup-closed diff-closed preBoolean set
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty cup-closed diff-closed preBoolean set
p is Element of CQC-WFF A
q is Element of bound_QC-variables A
r is Element of QC-WFF A
All (q,r) is Element of QC-WFF A
A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
proj2 A is finite set
len A is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
{ (A . b1) where b1 is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT : ( 1 <= b1 & b1 <= len A ) } is set
p is set
dom A is V56() V57() V58() V59() V60() V61() finite V74() V75() V76() Element of bool NAT
q is set
A . q is set
r is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
p is set
q is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
A . q is set
dom A is V56() V57() V58() V59() V60() V61() finite V74() V75() V76() Element of bool NAT
F2() is non empty set
F1() is non empty Relation-like QC-alphabet
QC-WFF F1() is non empty set
[:(QC-WFF F1()),F2():] is non empty Relation-like set
bool [:(QC-WFF F1()),F2():] is non empty cup-closed diff-closed preBoolean set
VERUM F1() is Element of CQC-WFF F1()
CQC-WFF F1() is non empty Element of bool (QC-WFF F1())
bool (QC-WFF F1()) is non empty cup-closed diff-closed preBoolean set
F3() is Element of F2()
A is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
A + 1 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
p is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
q is Element of QC-WFF F1()
@ q is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
QC-symbols F1() is non empty set
[:NAT,(QC-symbols F1()):] is non empty non trivial Relation-like non finite set
len (@ q) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
p . q is Element of F2()
F4(q) is Element of F2()
the_argument_of q is Element of QC-WFF F1()
p . (the_argument_of q) is Element of F2()
F5((p . (the_argument_of q)),q) is Element of F2()
the_left_argument_of q is Element of QC-WFF F1()
p . (the_left_argument_of q) is Element of F2()
the_right_argument_of q is Element of QC-WFF F1()
p . (the_right_argument_of q) is Element of F2()
F6((p . (the_left_argument_of q)),(p . (the_right_argument_of q)),q) is Element of F2()
the_scope_of q is Element of QC-WFF F1()
p . (the_scope_of q) is Element of F2()
F7((p . (the_scope_of q)),q) is Element of F2()
r is Element of F2()
r is Element of F2()
r is Element of F2()
r is Element of F2()
r is Element of F2()
r is Element of F2()
r is Element of F2()
f is Element of F2()
h is Element of F2()
u is Element of F2()
K is Element of F2()
f is Element of F2()
q is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
r is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
f is Element of QC-WFF F1()
@ f is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
QC-symbols F1() is non empty set
[:NAT,(QC-symbols F1()):] is non empty non trivial Relation-like non finite set
len (@ f) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
r . f is Element of F2()
F4(f) is Element of F2()
the_argument_of f is Element of QC-WFF F1()
r . (the_argument_of f) is Element of F2()
F5((r . (the_argument_of f)),f) is Element of F2()
the_left_argument_of f is Element of QC-WFF F1()
r . (the_left_argument_of f) is Element of F2()
the_right_argument_of f is Element of QC-WFF F1()
r . (the_right_argument_of f) is Element of F2()
F6((r . (the_left_argument_of f)),(r . (the_right_argument_of f)),f) is Element of F2()
the_scope_of f is Element of QC-WFF F1()
r . (the_scope_of f) is Element of F2()
F7((r . (the_scope_of f)),f) is Element of F2()
p . f is Element of F2()
p . f is Element of F2()
@ (the_argument_of f) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (the_argument_of f)) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
p . (the_argument_of f) is Element of F2()
p . f is Element of F2()
@ (the_right_argument_of f) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (the_right_argument_of f)) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
p . (the_right_argument_of f) is Element of F2()
@ (the_left_argument_of f) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (the_left_argument_of f)) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
p . (the_left_argument_of f) is Element of F2()
p . f is Element of F2()
@ (the_scope_of f) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (the_scope_of f)) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
p . (the_scope_of f) is Element of F2()
p . f is Element of F2()
0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative V35() V36() V37() V39() V40() V41() V42() V43() V44() V45() V46() V53() V54() V55() V56() V57() V58() V59() V60() V61() V62() finite finite-yielding V67() V74() V75() V76() V77() V78() V80( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V93() Element of NAT
the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
p is Element of QC-WFF F1()
@ p is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
QC-symbols F1() is non empty set
[:NAT,(QC-symbols F1()):] is non empty non trivial Relation-like non finite set
len (@ p) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . p is Element of F2()
F4(p) is Element of F2()
the_argument_of p is Element of QC-WFF F1()
the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . (the_argument_of p) is Element of F2()
F5(( the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . (the_argument_of p)),p) is Element of F2()
the_left_argument_of p is Element of QC-WFF F1()
the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . (the_left_argument_of p) is Element of F2()
the_right_argument_of p is Element of QC-WFF F1()
the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . (the_right_argument_of p) is Element of F2()
F6(( the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . (the_left_argument_of p)),( the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . (the_right_argument_of p)),p) is Element of F2()
the_scope_of p is Element of QC-WFF F1()
the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . (the_scope_of p) is Element of F2()
F7(( the non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():] . (the_scope_of p)),p) is Element of F2()
A is set
p is Element of QC-WFF F1()
@ p is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
QC-symbols F1() is non empty set
[:NAT,(QC-symbols F1()):] is non empty non trivial Relation-like non finite set
len (@ p) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
q . A is set
r is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
r . p is Element of F2()
f is Element of QC-WFF F1()
@ f is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ f) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . f is Element of F2()
r . f is Element of F2()
F4(f) is Element of F2()
@ (VERUM F1()) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (VERUM F1())) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . (VERUM F1()) is Element of F2()
r . (VERUM F1()) is Element of F2()
the_argument_of f is Element of QC-WFF F1()
@ (the_argument_of f) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (the_argument_of f)) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . (the_argument_of f) is Element of F2()
r . (the_argument_of f) is Element of F2()
F5((r . (the_argument_of f)),f) is Element of F2()
the_left_argument_of f is Element of QC-WFF F1()
@ (the_left_argument_of f) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (the_left_argument_of f)) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . (the_left_argument_of f) is Element of F2()
r . (the_left_argument_of f) is Element of F2()
the_right_argument_of f is Element of QC-WFF F1()
@ (the_right_argument_of f) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (the_right_argument_of f)) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . (the_right_argument_of f) is Element of F2()
r . (the_right_argument_of f) is Element of F2()
F6((r . (the_left_argument_of f)),(r . (the_right_argument_of f)),f) is Element of F2()
the_scope_of f is Element of QC-WFF F1()
@ (the_scope_of f) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (the_scope_of f)) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . (the_scope_of f) is Element of F2()
r . (the_scope_of f) is Element of F2()
F7((r . (the_scope_of f)),f) is Element of F2()
A is Relation-like Function-like set
proj1 A is set
proj2 A is set
p is set
q is set
A . q is set
r is Element of QC-WFF F1()
@ r is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
QC-symbols F1() is non empty set
[:NAT,(QC-symbols F1()):] is non empty non trivial Relation-like non finite set
len (@ r) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
f is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
f . r is Element of F2()
p is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
p . (VERUM F1()) is Element of F2()
q is Element of QC-WFF F1()
@ q is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
QC-symbols F1() is non empty set
[:NAT,(QC-symbols F1()):] is non empty non trivial Relation-like non finite set
len (@ q) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
r is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
r . (VERUM F1()) is Element of F2()
f is Element of QC-WFF F1()
p . f is Element of F2()
F4(f) is Element of F2()
the_argument_of f is Element of QC-WFF F1()
p . (the_argument_of f) is Element of F2()
F5((p . (the_argument_of f)),f) is Element of F2()
the_left_argument_of f is Element of QC-WFF F1()
p . (the_left_argument_of f) is Element of F2()
the_right_argument_of f is Element of QC-WFF F1()
p . (the_right_argument_of f) is Element of F2()
F6((p . (the_left_argument_of f)),(p . (the_right_argument_of f)),f) is Element of F2()
the_scope_of f is Element of QC-WFF F1()
p . (the_scope_of f) is Element of F2()
F7((p . (the_scope_of f)),f) is Element of F2()
h is Element of QC-WFF F1()
@ h is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ h) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u is non empty Relation-like QC-WFF F1() -defined F2() -valued Function-like total quasi_total Element of bool [:(QC-WFF F1()),F2():]
u . f is Element of F2()
@ f is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ f) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
f is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
r9 is Element of QC-WFF F1()
@ r9 is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ r9) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u . r9 is Element of F2()
F4(r9) is Element of F2()
the_argument_of r9 is Element of QC-WFF F1()
u . (the_argument_of r9) is Element of F2()
F5((u . (the_argument_of r9)),r9) is Element of F2()
the_left_argument_of r9 is Element of QC-WFF F1()
u . (the_left_argument_of r9) is Element of F2()
the_right_argument_of r9 is Element of QC-WFF F1()
u . (the_right_argument_of r9) is Element of F2()
F6((u . (the_left_argument_of r9)),(u . (the_right_argument_of r9)),r9) is Element of F2()
the_scope_of r9 is Element of QC-WFF F1()
u . (the_scope_of r9) is Element of F2()
F7((u . (the_scope_of r9)),r9) is Element of F2()
@ (the_argument_of f) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (the_argument_of f)) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
s9 is Element of QC-WFF F1()
@ s9 is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ s9) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u . s9 is Element of F2()
F4(s9) is Element of F2()
the_argument_of s9 is Element of QC-WFF F1()
u . (the_argument_of s9) is Element of F2()
F5((u . (the_argument_of s9)),s9) is Element of F2()
the_left_argument_of s9 is Element of QC-WFF F1()
u . (the_left_argument_of s9) is Element of F2()
the_right_argument_of s9 is Element of QC-WFF F1()
u . (the_right_argument_of s9) is Element of F2()
F6((u . (the_left_argument_of s9)),(u . (the_right_argument_of s9)),s9) is Element of F2()
the_scope_of s9 is Element of QC-WFF F1()
u . (the_scope_of s9) is Element of F2()
F7((u . (the_scope_of s9)),s9) is Element of F2()
u . (the_argument_of f) is Element of F2()
s9 is Element of QC-WFF F1()
@ s9 is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ s9) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
@ (the_left_argument_of f) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (the_left_argument_of f)) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
@ (the_right_argument_of f) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (the_right_argument_of f)) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u is Element of QC-WFF F1()
@ u is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ u) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u . u is Element of F2()
F4(u) is Element of F2()
the_argument_of u is Element of QC-WFF F1()
u . (the_argument_of u) is Element of F2()
F5((u . (the_argument_of u)),u) is Element of F2()
the_left_argument_of u is Element of QC-WFF F1()
u . (the_left_argument_of u) is Element of F2()
the_right_argument_of u is Element of QC-WFF F1()
u . (the_right_argument_of u) is Element of F2()
F6((u . (the_left_argument_of u)),(u . (the_right_argument_of u)),u) is Element of F2()
the_scope_of u is Element of QC-WFF F1()
u . (the_scope_of u) is Element of F2()
F7((u . (the_scope_of u)),u) is Element of F2()
u is Element of QC-WFF F1()
@ u is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ u) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u . u is Element of F2()
F4(u) is Element of F2()
the_argument_of u is Element of QC-WFF F1()
u . (the_argument_of u) is Element of F2()
F5((u . (the_argument_of u)),u) is Element of F2()
the_left_argument_of u is Element of QC-WFF F1()
u . (the_left_argument_of u) is Element of F2()
the_right_argument_of u is Element of QC-WFF F1()
u . (the_right_argument_of u) is Element of F2()
F6((u . (the_left_argument_of u)),(u . (the_right_argument_of u)),u) is Element of F2()
the_scope_of u is Element of QC-WFF F1()
u . (the_scope_of u) is Element of F2()
F7((u . (the_scope_of u)),u) is Element of F2()
u . (the_right_argument_of f) is Element of F2()
u is Element of QC-WFF F1()
@ u is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ u) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u . (the_left_argument_of f) is Element of F2()
u is Element of QC-WFF F1()
@ u is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ u) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
@ (the_scope_of f) is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ (the_scope_of f)) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
r9 is Element of QC-WFF F1()
@ r9 is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ r9) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
u . r9 is Element of F2()
F4(r9) is Element of F2()
the_argument_of r9 is Element of QC-WFF F1()
u . (the_argument_of r9) is Element of F2()
F5((u . (the_argument_of r9)),r9) is Element of F2()
the_left_argument_of r9 is Element of QC-WFF F1()
u . (the_left_argument_of r9) is Element of F2()
the_right_argument_of r9 is Element of QC-WFF F1()
u . (the_right_argument_of r9) is Element of F2()
F6((u . (the_left_argument_of r9)),(u . (the_right_argument_of r9)),r9) is Element of F2()
the_scope_of r9 is Element of QC-WFF F1()
u . (the_scope_of r9) is Element of F2()
F7((u . (the_scope_of r9)),r9) is Element of F2()
u . (the_scope_of f) is Element of F2()
r9 is Element of QC-WFF F1()
@ r9 is Relation-like NAT -defined [:NAT,(QC-symbols F1()):] -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of [:NAT,(QC-symbols F1()):]
len (@ r9) is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
F2() is non empty set
F3() is non empty set
Funcs (F2(),F3()) is non empty functional FUNCTION_DOMAIN of F2(),F3()
F1() is non empty Relation-like QC-alphabet
CQC-WFF F1() is non empty Element of bool (QC-WFF F1())
QC-WFF F1() is non empty set
bool (QC-WFF F1()) is non empty cup-closed diff-closed preBoolean set
[:(CQC-WFF F1()),(Funcs (F2(),F3())):] is non empty Relation-like set
bool [:(CQC-WFF F1()),(Funcs (F2(),F3())):] is non empty cup-closed diff-closed preBoolean set
VERUM F1() is Element of CQC-WFF F1()
F4() is Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of Funcs (F2(),F3())
bound_QC-variables F1() is non empty Element of bool (QC-variables F1())
QC-variables F1() is non empty set
bool (QC-variables F1()) is non empty cup-closed diff-closed preBoolean set
QC-pred_symbols F1() is non empty set
[:(QC-WFF F1()),(Funcs (F2(),F3())):] is non empty Relation-like set
bool [:(QC-WFF F1()),(Funcs (F2(),F3())):] is non empty cup-closed diff-closed preBoolean set
A is non empty Relation-like QC-WFF F1() -defined Funcs (F2(),F3()) -valued Function-like total quasi_total Function-yielding V93() Element of bool [:(QC-WFF F1()),(Funcs (F2(),F3())):]
A . (VERUM F1()) is Relation-like Function-like Element of Funcs (F2(),F3())
A | (CQC-WFF F1()) is Relation-like CQC-WFF F1() -defined QC-WFF F1() -defined Funcs (F2(),F3()) -valued Function-like Function-yielding V93() Element of bool [:(QC-WFF F1()),(Funcs (F2(),F3())):]
p is non empty Relation-like CQC-WFF F1() -defined Funcs (F2(),F3()) -valued Function-like total quasi_total Function-yielding V93() Element of bool [:(CQC-WFF F1()),(Funcs (F2(),F3())):]
p . (VERUM F1()) is Relation-like Function-like Element of Funcs (F2(),F3())
q is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q -ary_QC-pred_symbols F1() is non empty Element of bool (QC-pred_symbols F1())
bool (QC-pred_symbols F1()) is non empty cup-closed diff-closed preBoolean set
r is Relation-like NAT -defined bound_QC-variables F1() -valued QC-variables F1() -valued Function-like finite V80(q) FinSequence-like FinSubsequence-like FinSequence of QC-variables F1()
f is Element of q -ary_QC-pred_symbols F1()
f ! r is Element of CQC-WFF F1()
p . (f ! r) is Relation-like Function-like Element of Funcs (F2(),F3())
F5(q,f,r) is Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of Funcs (F2(),F3())
the_arity_of f is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
the_arguments_of (f ! r) is Relation-like NAT -defined QC-variables F1() -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of QC-variables F1()
the_pred_symbol_of (f ! r) is Element of QC-pred_symbols F1()
A . (f ! r) is Relation-like Function-like Element of Funcs (F2(),F3())
q is Element of CQC-WFF F1()
'not' q is Element of CQC-WFF F1()
p . ('not' q) is Relation-like Function-like Element of Funcs (F2(),F3())
p . q is Relation-like Function-like Element of Funcs (F2(),F3())
F6((p . q),q) is Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of Funcs (F2(),F3())
r is Element of CQC-WFF F1()
q '&' r is Element of CQC-WFF F1()
p . (q '&' r) is Relation-like Function-like Element of Funcs (F2(),F3())
p . r is Relation-like Function-like Element of Funcs (F2(),F3())
F7((p . q),(p . r),q,r) is Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of Funcs (F2(),F3())
f is Element of bound_QC-variables F1()
All (f,q) is Element of CQC-WFF F1()
p . (All (f,q)) is Relation-like Function-like Element of Funcs (F2(),F3())
F8(f,(p . q),q) is Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of Funcs (F2(),F3())
A . q is Relation-like Function-like Element of Funcs (F2(),F3())
the_argument_of ('not' q) is Element of QC-WFF F1()
A . ('not' q) is Relation-like Function-like Element of Funcs (F2(),F3())
A . r is Relation-like Function-like Element of Funcs (F2(),F3())
the_left_argument_of (q '&' r) is Element of QC-WFF F1()
the_right_argument_of (q '&' r) is Element of QC-WFF F1()
A . (q '&' r) is Relation-like Function-like Element of Funcs (F2(),F3())
bound_in (All (f,q)) is Element of bound_QC-variables F1()
the_scope_of (All (f,q)) is Element of QC-WFF F1()
A . (All (f,q)) is Relation-like Function-like Element of Funcs (F2(),F3())
F1() is non empty Relation-like QC-alphabet
CQC-WFF F1() is non empty Element of bool (QC-WFF F1())
QC-WFF F1() is non empty set
bool (QC-WFF F1()) is non empty cup-closed diff-closed preBoolean set
F2() is non empty set
F3() is non empty set
Funcs (F2(),F3()) is non empty functional FUNCTION_DOMAIN of F2(),F3()
[:(CQC-WFF F1()),(Funcs (F2(),F3())):] is non empty Relation-like set
bool [:(CQC-WFF F1()),(Funcs (F2(),F3())):] is non empty cup-closed diff-closed preBoolean set
[:F2(),F3():] is non empty Relation-like set
bool [:F2(),F3():] is non empty cup-closed diff-closed preBoolean set
F4() is non empty Relation-like CQC-WFF F1() -defined Funcs (F2(),F3()) -valued Function-like total quasi_total Function-yielding V93() Element of bool [:(CQC-WFF F1()),(Funcs (F2(),F3())):]
VERUM F1() is Element of CQC-WFF F1()
F4() . (VERUM F1()) is Relation-like Function-like Element of Funcs (F2(),F3())
F6() is non empty Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of bool [:F2(),F3():]
bound_QC-variables F1() is non empty Element of bool (QC-variables F1())
QC-variables F1() is non empty set
bool (QC-variables F1()) is non empty cup-closed diff-closed preBoolean set
QC-pred_symbols F1() is non empty set
F5() is non empty Relation-like CQC-WFF F1() -defined Funcs (F2(),F3()) -valued Function-like total quasi_total Function-yielding V93() Element of bool [:(CQC-WFF F1()),(Funcs (F2(),F3())):]
F5() . (VERUM F1()) is Relation-like Function-like Element of Funcs (F2(),F3())
F4() . (VERUM F1()) is Relation-like Function-like set
F5() . (VERUM F1()) is Relation-like Function-like set
A is Element of CQC-WFF F1()
F4() . A is Relation-like Function-like set
F5() . A is Relation-like Function-like set
'not' A is Element of CQC-WFF F1()
F4() . ('not' A) is Relation-like Function-like set
F5() . ('not' A) is Relation-like Function-like set
p is Element of CQC-WFF F1()
F4() . p is Relation-like Function-like set
F5() . p is Relation-like Function-like set
A '&' p is Element of CQC-WFF F1()
F4() . (A '&' p) is Relation-like Function-like set
F5() . (A '&' p) is Relation-like Function-like set
q is Element of bound_QC-variables F1()
All (q,A) is Element of CQC-WFF F1()
F4() . (All (q,A)) is Relation-like Function-like set
F5() . (All (q,A)) is Relation-like Function-like set
r is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
r -ary_QC-pred_symbols F1() is non empty Element of bool (QC-pred_symbols F1())
bool (QC-pred_symbols F1()) is non empty cup-closed diff-closed preBoolean set
f is Relation-like NAT -defined bound_QC-variables F1() -valued QC-variables F1() -valued Function-like finite V80(r) FinSequence-like FinSubsequence-like FinSequence of QC-variables F1()
h is Element of r -ary_QC-pred_symbols F1()
h ! f is Element of CQC-WFF F1()
F4() . (h ! f) is Relation-like Function-like set
F5() . (h ! f) is Relation-like Function-like set
F4() . (h ! f) is Relation-like Function-like Element of Funcs (F2(),F3())
F7(r,h,f) is non empty Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of bool [:F2(),F3():]
F5() . (h ! f) is Relation-like Function-like Element of Funcs (F2(),F3())
F4() . ('not' A) is Relation-like Function-like Element of Funcs (F2(),F3())
F4() . A is Relation-like Function-like Element of Funcs (F2(),F3())
F8((F4() . A),A) is non empty Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of bool [:F2(),F3():]
F5() . A is Relation-like Function-like Element of Funcs (F2(),F3())
F5() . ('not' A) is Relation-like Function-like Element of Funcs (F2(),F3())
F4() . (A '&' p) is Relation-like Function-like Element of Funcs (F2(),F3())
F4() . p is Relation-like Function-like Element of Funcs (F2(),F3())
F9((F4() . A),(F4() . p),A,p) is non empty Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of bool [:F2(),F3():]
F5() . p is Relation-like Function-like Element of Funcs (F2(),F3())
F5() . (A '&' p) is Relation-like Function-like Element of Funcs (F2(),F3())
F4() . (All (q,A)) is Relation-like Function-like Element of Funcs (F2(),F3())
F10(q,(F4() . A),A) is non empty Relation-like F2() -defined F3() -valued Function-like total quasi_total Element of bool [:F2(),F3():]
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is non empty cup-closed diff-closed preBoolean set
p is Element of CQC-WFF A
'not' p is Element of CQC-WFF A
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is non empty cup-closed diff-closed preBoolean set
p is Element of CQC-WFF A
q is Element of CQC-WFF A
p '&' q is Element of CQC-WFF A
A is non empty Relation-like QC-alphabet
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool (QC-WFF A)
bool (QC-WFF A) is non empty cup-closed diff-closed preBoolean set
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty cup-closed diff-closed preBoolean set
p is Element of CQC-WFF A
q is Element of bound_QC-variables A
All (q,p) is Element of CQC-WFF A
A is non empty Relation-like QC-alphabet
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is non empty cup-closed diff-closed preBoolean set
p is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q is Relation-like NAT -defined bound_QC-variables A -valued QC-variables A -valued Function-like finite V80(p) FinSequence-like FinSubsequence-like FinSequence of QC-variables A
len q is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
r is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
q . r is set
dom q is V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V80(p) Element of bool NAT
proj2 q is finite set
p is non empty set
A is non empty Relation-like QC-alphabet
CQC-WFF A is non empty Element of bool (QC-WFF A)
QC-WFF A is non empty set
bool (QC-WFF A) is non empty cup-closed diff-closed preBoolean set
[:p,(CQC-WFF A):] is non empty Relation-like set
bool [:p,(CQC-WFF A):] is non empty cup-closed diff-closed preBoolean set
Funcs (p,(CQC-WFF A)) is non empty functional FUNCTION_DOMAIN of p, CQC-WFF A
q is non empty Relation-like p -defined CQC-WFF A -valued Function-like total quasi_total Element of bool [:p,(CQC-WFF A):]
r is Element of p
q . r is set
q . r is Element of CQC-WFF A
f is Element of CQC-WFF A
'not' f is Element of CQC-WFF A
h is Element of CQC-WFF A
'not' h is Element of CQC-WFF A
r is non empty Relation-like p -defined CQC-WFF A -valued Function-like total quasi_total Element of bool [:p,(CQC-WFF A):]
r is Relation-like p -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs (p,(CQC-WFF A))
f is Relation-like p -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs (p,(CQC-WFF A))
h is Element of p
r . h is Element of CQC-WFF A
f . h is Element of CQC-WFF A
q . h is Element of CQC-WFF A
u is Element of CQC-WFF A
'not' u is Element of CQC-WFF A
A is non empty Relation-like QC-alphabet
QC-symbols A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is non empty cup-closed diff-closed preBoolean set
Funcs ((bound_QC-variables A),(bound_QC-variables A)) is non empty functional FUNCTION_DOMAIN of bound_QC-variables A, bound_QC-variables A
[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] is non empty Relation-like set
CQC-WFF A is non empty Element of bool (QC-WFF A)
QC-WFF A is non empty set
bool (QC-WFF A) is non empty cup-closed diff-closed preBoolean set
[:[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A):] is non empty Relation-like set
bool [:[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A):] is non empty cup-closed diff-closed preBoolean set
Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) is non empty functional FUNCTION_DOMAIN of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):], CQC-WFF A
p is non empty Relation-like [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] -defined CQC-WFF A -valued Function-like total quasi_total Element of bool [:[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A):]
q is non empty Relation-like [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] -defined CQC-WFF A -valued Function-like total quasi_total Element of bool [:[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A):]
r is ext-real non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V74() V75() V76() V78() Element of NAT
f is Element of QC-symbols A
f + r is Element of QC-symbols A
h is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like total quasi_total Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
[f,h] is V18() set
{f,h} is non empty finite set
{f} is non empty trivial finite V80(1) set
{{f,h},{f}} is non empty finite V67() set
p . [f,h] is set
[(f + r),h] is V18() set
{(f + r),h} is non empty finite set
{(f + r)} is non empty trivial finite V80(1) set
{{(f + r),h},{(f + r)}} is non empty finite V67() set
q . [(f + r),h] is set
[f,h] is V18() Element of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):]
p . [f,h] is Element of CQC-WFF A
[(f + r),h] is V18() Element of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):]
q . [(f + r),h] is Element of CQC-WFF A
u is Element of CQC-WFF A
K is Element of CQC-WFF A
u '&' K is Element of CQC-WFF A
f is Element of CQC-WFF A
r9 is Element of CQC-WFF A
f '&' r9 is Element of CQC-WFF A
f is non empty Relation-like [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] -defined CQC-WFF A -valued Function-like total quasi_total Element of bool [:[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A):]
h is Relation-like [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))
u is Element of QC-symbols A
u + r is Element of QC-symbols A
K is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like total quasi_total Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
p . (u,K) is Element of CQC-WFF A
[u,K] is V18() set
{u,K} is non empty finite set
{u} is non empty trivial finite V80(1) set
{{u,K},{u}} is non empty finite V67() set
p . [u,K] is set
q . ((u + r),K) is Element of CQC-WFF A
[(u + r),K] is V18() set
{(u + r),K} is non empty finite set
{(u + r)} is non empty trivial finite V80(1) set
{{(u + r),K},{(u + r)}} is non empty finite V67() set
q . [(u + r),K] is set
h . (u,K) is Element of CQC-WFF A
h . [u,K] is set
f is Element of CQC-WFF A
r9 is Element of CQC-WFF A
f '&' r9 is Element of CQC-WFF A
f is Relation-like [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))
h is Relation-like [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))
u is Element of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):]
f . u is Element of CQC-WFF A
h . u is Element of CQC-WFF A
K is Element of QC-symbols A
f is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like total quasi_total Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
[K,f] is V18() Element of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):]
{K,f} is non empty finite set
{K} is non empty trivial finite V80(1) set
{{K,f},{K}} is non empty finite V67() set
K + r is Element of QC-symbols A
q . ((K + r),f) is Element of CQC-WFF A
[(K + r),f] is V18() set
{(K + r),f} is non empty finite set
{(K + r)} is non empty trivial finite V80(1) set
{{(K + r),f},{(K + r)}} is non empty finite V67() set
q . [(K + r),f] is set
p . (K,f) is Element of CQC-WFF A
[K,f] is V18() set
p . [K,f] is set
f . (K,f) is Element of CQC-WFF A
f . [K,f] is set
s9 is Element of CQC-WFF A
r9 is Element of CQC-WFF A
s9 '&' r9 is Element of CQC-WFF A
h . (K,f) is Element of CQC-WFF A
h . [K,f] is set
A is non empty Relation-like QC-alphabet
QC-symbols A is non empty set
QC-variables A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
bool (QC-variables A) is non empty cup-closed diff-closed preBoolean set
Funcs ((bound_QC-variables A),(bound_QC-variables A)) is non empty functional FUNCTION_DOMAIN of bound_QC-variables A, bound_QC-variables A
[:(bound_QC-variables A),(bound_QC-variables A):] is non empty Relation-like set
bool [:(bound_QC-variables A),(bound_QC-variables A):] is non empty cup-closed diff-closed preBoolean set
p is Element of QC-symbols A
x. p is Element of bound_QC-variables A
4 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
[4,p] is V18() set
{4,p} is non empty finite set
{4} is non empty trivial V56() V57() V58() V59() V60() V61() finite V67() V72() V73() V74() V75() V76() V80(1) set
{{4,p},{4}} is non empty finite V67() set
q is Element of bound_QC-variables A
q .--> (x. p) is Relation-like bound_QC-variables A -defined {q} -defined bound_QC-variables A -valued Function-like one-to-one finite set
{q} is non empty trivial finite V80(1) set
{q} --> (x. p) is non empty Relation-like {q} -defined bound_QC-variables A -valued {(x. p)} -valued Function-like constant total quasi_total finite Element of bool [:{q},{(x. p)}:]
{(x. p)} is non empty trivial finite V80(1) set
[:{q},{(x. p)}:] is non empty Relation-like finite set
bool [:{q},{(x. p)}:] is non empty cup-closed diff-closed preBoolean finite V67() set
r is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like total quasi_total Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
r +* (q .--> (x. p)) is Relation-like Function-like set
proj2 (r +* (q .--> (x. p))) is set
proj2 r is set
proj2 (q .--> (x. p)) is finite set
(proj2 r) \/ (proj2 (q .--> (x. p))) is set
proj1 (r +* (q .--> (x. p))) is set
proj1 r is set
{q} is non empty trivial finite V80(1) Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty cup-closed diff-closed preBoolean set
{q} --> (x. p) is non empty Relation-like {q} -defined bound_QC-variables A -valued Function-like constant total quasi_total finite Element of bool [:{q},(bound_QC-variables A):]
[:{q},(bound_QC-variables A):] is non empty Relation-like set
bool [:{q},(bound_QC-variables A):] is non empty cup-closed diff-closed preBoolean set
[:{q},{(x. p)}:] is non empty Relation-like finite set
proj1 ({q} --> (x. p)) is non empty finite set
(proj1 r) \/ (proj1 ({q} --> (x. p))) is non empty set
(proj1 r) \/ {q} is non empty set
(bound_QC-variables A) \/ {q} is non empty set
A is non empty Relation-like QC-alphabet
QC-symbols A is non empty set
bound_QC-variables A is non empty Element of bool (QC-variables A)
QC-variables A is non empty set
bool (QC-variables A) is non empty cup-closed diff-closed preBoolean set
Funcs ((bound_QC-variables A),(bound_QC-variables A)) is non empty functional FUNCTION_DOMAIN of bound_QC-variables A, bound_QC-variables A
[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] is non empty Relation-like set
CQC-WFF A is non empty Element of bool (QC-WFF A)
QC-WFF A is non empty set
bool (QC-WFF A) is non empty cup-closed diff-closed preBoolean set
[:[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A):] is non empty Relation-like set
bool [:[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A):] is non empty cup-closed diff-closed preBoolean set
Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) is non empty functional FUNCTION_DOMAIN of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):], CQC-WFF A
p is non empty Relation-like [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] -defined CQC-WFF A -valued Function-like total quasi_total Element of bool [:[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A):]
q is Element of bound_QC-variables A
{q} is non empty trivial finite V80(1) Element of bool (bound_QC-variables A)
bool (bound_QC-variables A) is non empty cup-closed diff-closed preBoolean set
r is Element of QC-symbols A
r ++ is Element of QC-symbols A
x. r is Element of bound_QC-variables A
4 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
[4,r] is V18() set
{4,r} is non empty finite set
{4} is non empty trivial V56() V57() V58() V59() V60() V61() finite V67() V72() V73() V74() V75() V76() V80(1) set
{{4,r},{4}} is non empty finite V67() set
{q} --> (x. r) is non empty Relation-like {q} -defined bound_QC-variables A -valued Function-like constant total quasi_total finite Element of bool [:{q},(bound_QC-variables A):]
[:{q},(bound_QC-variables A):] is non empty Relation-like set
bool [:{q},(bound_QC-variables A):] is non empty cup-closed diff-closed preBoolean set
{(x. r)} is non empty trivial finite V80(1) set
[:{q},{(x. r)}:] is non empty Relation-like finite set
f is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like total quasi_total Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
f +* ({q} --> (x. r)) is Relation-like Function-like set
[(r ++),(f +* ({q} --> (x. r)))] is V18() set
{(r ++),(f +* ({q} --> (x. r)))} is non empty finite set
{(r ++)} is non empty trivial finite V80(1) set
{{(r ++),(f +* ({q} --> (x. r)))},{(r ++)}} is non empty finite V67() set
p . [(r ++),(f +* ({q} --> (x. r)))] is set
[:(bound_QC-variables A),(bound_QC-variables A):] is non empty Relation-like set
bool [:(bound_QC-variables A),(bound_QC-variables A):] is non empty cup-closed diff-closed preBoolean set
q .--> (x. r) is Relation-like bound_QC-variables A -defined {q} -defined bound_QC-variables A -valued Function-like one-to-one finite set
{q} is non empty trivial finite V80(1) set
{q} --> (x. r) is non empty Relation-like {q} -defined bound_QC-variables A -valued {(x. r)} -valued Function-like constant total quasi_total finite Element of bool [:{q},{(x. r)}:]
[:{q},{(x. r)}:] is non empty Relation-like finite set
bool [:{q},{(x. r)}:] is non empty cup-closed diff-closed preBoolean finite V67() set
f +* (q .--> (x. r)) is Relation-like Function-like set
h is non empty Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like total quasi_total Element of bool [:(bound_QC-variables A),(bound_QC-variables A):]
u is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like total quasi_total Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
[(r ++),u] is V18() Element of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):]
{(r ++),u} is non empty finite set
{{(r ++),u},{(r ++)}} is non empty finite V67() set
p . [(r ++),u] is Element of CQC-WFF A
K is Element of CQC-WFF A
All ((x. r),K) is Element of CQC-WFF A
f is Element of CQC-WFF A
All ((x. r),f) is Element of CQC-WFF A
r is non empty Relation-like [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] -defined CQC-WFF A -valued Function-like total quasi_total Element of bool [:[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A):]
f is Relation-like [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))
h is Element of QC-symbols A
h ++ is Element of QC-symbols A
x. h is Element of bound_QC-variables A
4 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74() V75() V76() V78() Element of NAT
[4,h] is V18() set
{4,h} is non empty finite set
{4} is non empty trivial V56() V57() V58() V59() V60() V61() finite V67() V72() V73() V74() V75() V76() V80(1) set
{{4,h},{4}} is non empty finite V67() set
q .--> (x. h) is Relation-like bound_QC-variables A -defined {q} -defined bound_QC-variables A -valued Function-like one-to-one finite set
{q} is non empty trivial finite V80(1) set
{q} --> (x. h) is non empty Relation-like {q} -defined bound_QC-variables A -valued {(x. h)} -valued Function-like constant total quasi_total finite Element of bool [:{q},{(x. h)}:]
{(x. h)} is non empty trivial finite V80(1) set
[:{q},{(x. h)}:] is non empty Relation-like finite set
bool [:{q},{(x. h)}:] is non empty cup-closed diff-closed preBoolean finite V67() set
u is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like total quasi_total Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
u +* (q .--> (x. h)) is Relation-like Function-like set
p . ((h ++),(u +* (q .--> (x. h)))) is set
[(h ++),(u +* (q .--> (x. h)))] is V18() set
{(h ++),(u +* (q .--> (x. h)))} is non empty finite set
{(h ++)} is non empty trivial finite V80(1) set
{{(h ++),(u +* (q .--> (x. h)))},{(h ++)}} is non empty finite V67() set
p . [(h ++),(u +* (q .--> (x. h)))] is set
f . (h,u) is Element of CQC-WFF A
[h,u] is V18() set
{h,u} is non empty finite set
{h} is non empty trivial finite V80(1) set
{{h,u},{h}} is non empty finite V67() set
f . [h,u] is set
K is Element of CQC-WFF A
All ((x. h),K) is Element of CQC-WFF A
r is Relation-like [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))
f is Relation-like [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] -defined CQC-WFF A -valued Function-like total quasi_total Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))
h is Element of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):]
r . h is Element of CQC-WFF A
f . h is Element of CQC-WFF A
u is Element of QC-symbols A
K is Relation-like bound_QC-variables A -defined bound_QC-variables A -valued Function-like total quasi_total Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
[u,K] is V18() Element of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):]
{u,K} is non empty finite set
{u} is non empty trivial finite V80(1) set
{{u,K},{u}} is non empty finite V67() set
[:(bound_QC-variables A),(bound_QC-variables A):] is non empty Relation-like set
bool [:(bound_QC-variables A),(bound_QC-variables A):] is non empty cup-closed diff-closed preBoolean set
x. u is Element of bound_QC-variables A
4 is non empty ext-real positive non negative V35() V36() V37() V41() V42() V53() V54() V55() V56() V57() V58() V59() V60() V61() finite V72() V73() V74()