:: SUBSTUT1 semantic presentation

REAL is V45() V46() V47() V51() set
NAT is non empty non trivial V21() V22() V23() V45() V46() V47() V48() V49() V50() V51() non finite cardinal limit_cardinal V94() V95() Element of bool REAL
bool REAL is non empty set
COMPLEX is V45() V51() set
RAT is V45() V46() V47() V48() V51() set
INT is V45() V46() V47() V48() V49() V51() set
NAT is non empty non trivial V21() V22() V23() V45() V46() V47() V48() V49() V50() V51() non finite cardinal limit_cardinal V94() V95() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set

bool is non empty set

bool is non empty set
{} is Function-like functional empty ext-real non positive non negative V21() V22() V23() V25() V26() V27() V45() V46() V47() V48() V49() V50() V51() finite V56() cardinal {} -element FinSequence-membered V94() set
1 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
2 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
3 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
Seg 1 is non empty trivial V45() V46() V47() V48() V49() V50() finite 1 -element V94() Element of bool NAT
0 is Function-like functional empty ext-real non positive non negative V21() V22() V23() V25() V26() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() V51() finite V56() cardinal {} -element FinSequence-membered V94() Element of NAT
[0,0] is V15() set
{0,0} is non empty V45() V46() V47() V48() V49() V50() finite V56() V94() set
is non empty trivial V45() V46() V47() V48() V49() V50() finite V56() 1 -element V94() set
is non empty finite V56() V94() set

[1,0] is V15() set
{1,0} is non empty V45() V46() V47() V48() V49() V50() finite V56() V94() set
{1} is non empty trivial V45() V46() V47() V48() V49() V50() finite V56() 1 -element V94() set
{{1,0},{1}} is non empty finite V56() V94() set

[2,0] is V15() set
{2,0} is non empty V45() V46() V47() V48() V49() V50() finite V56() V94() set
{2} is non empty trivial V45() V46() V47() V48() V49() V50() finite V56() 1 -element V94() set
{{2,0},{2}} is non empty finite V56() V94() set

[3,0] is V15() set
{3,0} is non empty V45() V46() V47() V48() V49() V50() finite V56() V94() set
{3} is non empty trivial V45() V46() V47() V48() V49() V50() finite V56() 1 -element V94() set
{{3,0},{3}} is non empty finite V56() V94() set

card NAT is non empty non trivial V21() V22() V23() non finite cardinal set

bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
6 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
{6} is non empty trivial V45() V46() V47() V48() V49() V50() finite V56() 1 -element V94() set
is non empty non trivial non finite set
4 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
5 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
{4,5} is non empty V45() V46() V47() V48() V49() V50() finite V56() V94() set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
{4} is non empty trivial V45() V46() V47() V48() V49() V50() finite V56() 1 -element V94() set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set

(A) is set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set

(A) is non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set

(A) is functional non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set
S is Relation-like Function-like Element of (A)
is non empty set
bool is non empty set

(A) is functional non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set
S is set
SQ is Relation-like Function-like Element of (A)
proj1 SQ is set
SQ . S is set

is non empty set
bool is non empty set
dom (A,SQ) is Element of bool
bool is non empty set

QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
(A) is functional non empty set
bound_QC-variables A is non empty Element of bool ()
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set

len S is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
SQ is Relation-like Function-like Element of (A)
proj1 SQ is set
Seg (len S) is V45() V46() V47() V48() V49() V50() finite len S -element V94() Element of bool NAT
S9 is ext-real V21() V22() V23() V27() finite cardinal V94() set
S . S9 is set
SQ . (S . S9) is set
S9 is set

dom S9 is V45() V46() V47() V48() V49() V50() finite V94() Element of bool NAT
proj2 S9 is finite V94() set
S9 is set
l is set
S9 . l is set
l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
S . l is set
S9 . l is set
SQ . (S . l) is set
l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
S . l is set
dom S is V45() V46() V47() V48() V49() V50() finite V94() Element of bool NAT
rng S is finite V94() Element of bool ()
S9 . l is set
l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
S . l is set
S9 . l is set
l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
S . l is set
S9 . l is set

len S9 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
S . l is set
S9 . l is set
SQ . (S . l) is set
dom S is V45() V46() V47() V48() V49() V50() finite V94() Element of bool NAT

len S9 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

len S9 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
l is ext-real V21() V22() V23() V27() finite cardinal V94() set
S . l is set
S9 . l is set
SQ . (S . l) is set
S9 . l is set

bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set

rng S is finite V94() Element of bool
bool is non empty set

bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
(A) is functional non empty set
PFuncs (,) is functional non empty set

SQ is Relation-like Function-like Element of (A)

len (A,(A,S),SQ) is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
len (A,S) is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
dom (A,(A,S),SQ) is V45() V46() V47() V48() V49() V50() finite V94() Element of bool NAT
Seg (len (A,S)) is V45() V46() V47() V48() V49() V50() finite len (A,S) -element V94() Element of bool NAT
proj1 SQ is set
S9 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
(A,S) . S9 is set
(A,(A,S),SQ) . S9 is set
SQ . ((A,S) . S9) is set
rng (A,(A,S),SQ) is finite V94() Element of bool ()
S9 is set
S9 is set
(A,(A,S),SQ) . S9 is set
l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
(A,S) . l is set
(A,(A,S),SQ) . l is set
SQ . ((A,S) . l) is set
l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
(A,S) . l is set
rng S is finite V94() Element of bool
bool is non empty set
dom (A,S) is V45() V46() V47() V48() V49() V50() finite V94() Element of bool NAT
rng (A,S) is finite V94() Element of bool ()
(A,(A,S),SQ) . l is set
l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
(A,S) . l is set
(A,(A,S),SQ) . l is set
l is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
(A,S) . l is set
(A,(A,S),SQ) . l is set

(A) is functional non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set
S is Relation-like Function-like Element of (A)
SQ is set

is non empty set
bool is non empty set

(A) is functional non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set
S is Function-like functional empty ext-real non positive non negative V21() V22() V23() V25() V26() V27() V45() V46() V47() V48() V49() V50() V51() finite V56() cardinal {} -element FinSequence-membered V94() set
is non empty set
bool is non empty set

QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bound_QC-variables A is non empty Element of bool ()
bool () is non empty set
[:{4},():] is non empty set
QC-WFF A is non empty set
(A) is functional non empty set
PFuncs (,) is functional non empty set
S9 is Relation-like Function-like Element of (A)
SQ is Element of QC-WFF A

bool is non empty set
proj1 S9 is set

{ b1 where b1 is Element of bound_QC-variables A : ( b1 in still_not-bound_in SQ & b1 is Element of proj1 S9 & not b1 = S & not b1 = S9 . b1 ) } is set
(A,S9, { b1 where b1 is Element of bound_QC-variables A : ( b1 in still_not-bound_in SQ & b1 is Element of proj1 S9 & not b1 = S & not b1 = S9 . b1 ) } ) is Relation-like Function-like Element of (A)
{ b1 where b1 is Element of bound_QC-variables A : ( b1 is Element of proj1 S9 & not b1 = S & not b1 = S9 . b1 ) } is set
l is finite V94() set
l /\ { b1 where b1 is Element of bound_QC-variables A : ( b1 is Element of proj1 S9 & not b1 = S & not b1 = S9 . b1 ) } is finite V94() set
s is set
P9 is Element of bound_QC-variables A
S9 . P9 is set
P9 is Element of bound_QC-variables A
S9 . P9 is set
s is finite V94() set
(A,S9,s) is Relation-like Function-like finite V94() Element of (A)

QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set

len S is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
bound_QC-variables A is non empty Element of bool ()
bool () is non empty set
[:{4},():] is non empty set
{ (S . b1) where b1 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT : ( 1 <= b1 & b1 <= len S & S . b1 in bound_QC-variables A ) } is set
bool is non empty set
S9 is set
S9 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
S . S9 is set

QC-WFF A is non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
bool is non empty set
[:(),():] is non empty set
bool [:(),():] is non empty set
S is Element of QC-WFF A
VERUM A is Element of CQC-WFF A
CQC-WFF A is non empty Element of bool ()
bool () is non empty set

QC-WFF A is non empty set
VERUM A is Element of CQC-WFF A
CQC-WFF A is non empty Element of bool ()
bool () is non empty set
(A,()) is Element of bool
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
bool is non empty set

S is Element of QC-WFF A
(A,S) is Element of bool

(A,()) is Element of bool
len () is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
{ (() . b1) where b1 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT : ( 1 <= b1 & b1 <= len () & () . b1 in bound_QC-variables A ) } is set

(A,()) is Element of bool

(A,) is Element of bool

(A,) is Element of bool
(A,) \/ (A,) is Element of bool

(A,()) is Element of bool

{()} is non empty trivial finite 1 -element V94() Element of bool
(A,()) \/ {()} is non empty Element of bool
[:(),():] is non empty set
bool [:(),():] is non empty set
S9 is Element of bool
S9 is Element of QC-WFF A
(A,S9) is Element of bool
l is Element of bool

l is Element of QC-WFF A
s . l is Element of bool
(A,l) is Element of bool
H2( the_scope_of S) \/ {()} is non empty Element of bool

VERUM A is Element of CQC-WFF A
QC-WFF A is non empty set
CQC-WFF A is non empty Element of bool ()
bool () is non empty set
(A,()) is Element of bool
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
bool is non empty set

QC-WFF A is non empty set
S is Element of QC-WFF A
(A,S) is Element of bool
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
bool is non empty set

(A,()) is Element of bool
len () is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
{ (() . b1) where b1 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT : ( 1 <= b1 & b1 <= len () & () . b1 in bound_QC-variables A ) } is set

QC-WFF A is non empty set
S is Element of QC-WFF A
(A,S) is Element of bool
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
bool is non empty set

(A,()) is Element of bool

QC-WFF A is non empty set
S is Element of QC-WFF A
(A,S) is Element of bool
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
bool is non empty set

(A,) is Element of bool

(A,) is Element of bool
(A,) \/ (A,) is Element of bool

QC-WFF A is non empty set
S is Element of QC-WFF A
(A,S) is Element of bool
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
bool is non empty set

(A,()) is Element of bool

{()} is non empty trivial finite 1 -element V94() Element of bool
(A,()) \/ {()} is non empty Element of bool

QC-WFF A is non empty set
S is Element of QC-WFF A
(A,S) is Element of bool
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
bool is non empty set
VERUM A is Element of CQC-WFF A
CQC-WFF A is non empty Element of bool ()
bool () is non empty set
(A,()) is Element of bool
SQ is Element of QC-WFF A
(A,SQ) is Element of bool
the_argument_of SQ is Element of QC-WFF A
(A,()) is Element of bool

(A,()) is Element of bool

(A,) is Element of bool
the_scope_of SQ is Element of QC-WFF A
(A,()) is Element of bool

len () is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
S9 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
() . S9 is set
{ H1(b1) where b1 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT : S3[b1] } is set
{ H1(b1) where b1 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT : S2[b1] } is set
(A,()) is Element of bool
{ (() . b1) where b1 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT : ( 1 <= b1 & b1 <= len () & () . b1 in bound_QC-variables A ) } is set
rng () is finite V94() Element of bool ()
(A,()) \/ (A,) is Element of bool

{(bound_in SQ)} is non empty trivial finite 1 -element V94() Element of bool
(A,()) \/ {(bound_in SQ)} is non empty Element of bool

QC-WFF A is non empty set
QC-symbols A is non empty set
proj2 A is set
S is Element of QC-WFF A
(A,S) is finite V94() Element of bool
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
bool is non empty set
{ b1 where b1 is Element of QC-symbols A : x. b1 in (A,S) } is set
bool () is non empty set
S9 is set
S9 is Element of QC-symbols A
x. S9 is Element of bound_QC-variables A
[4,S9] is V15() set
{4,S9} is non empty finite V94() set
{{4,S9},{4}} is non empty finite V56() V94() set
S9 is set
S9 is Element of QC-symbols A
x. S9 is Element of bound_QC-variables A
[4,S9] is V15() set
{4,S9} is non empty finite V94() set
{{4,S9},{4}} is non empty finite V56() V94() set

proj1 S9 is set
S9 | { b1 where b1 is Element of QC-symbols A : x. b1 in (A,S) } is Relation-like Function-like set
proj2 (S9 | { b1 where b1 is Element of QC-symbols A : x. b1 in (A,S) } ) is set
S9 is set
proj1 (S9 | { b1 where b1 is Element of QC-symbols A : x. b1 in (A,S) } ) is set
l is set
(S9 | { b1 where b1 is Element of QC-symbols A : x. b1 in (A,S) } ) . l is set
S9 . l is set
l is Element of QC-symbols A

[4,l] is V15() set
{4,l} is non empty finite V94() set
{{4,l},{4}} is non empty finite V56() V94() set
s is Element of QC-symbols A

[4,s] is V15() set
{4,s} is non empty finite V94() set
{{4,s},{4}} is non empty finite V56() V94() set
S9 is set
l is set
S9 . S9 is set
S9 . l is set
l is Element of QC-symbols A

[4,l] is V15() set
{4,l} is non empty finite V94() set
{{4,l},{4}} is non empty finite V56() V94() set
s is Element of QC-symbols A

[4,s] is V15() set
{4,s} is non empty finite V94() set
{{4,s},{4}} is non empty finite V56() V94() set
proj1 (S9 | { b1 where b1 is Element of QC-symbols A : x. b1 in (A,S) } ) is set
S9 is Element of bool ()

proj1 (S9 | S9) is set
l is set
l is set
S9 /\ () is Element of bool ()

(A) is functional non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set
S is Relation-like Function-like finite V94() Element of (A)
proj2 S is finite V94() set
{ b1 where b1 is Element of QC-symbols A : x. b1 in proj2 S } is set
bool () is non empty set
S9 is set
S9 is Element of QC-symbols A
x. S9 is Element of bound_QC-variables A
[4,S9] is V15() set
{4,S9} is non empty finite V94() set
{{4,S9},{4}} is non empty finite V56() V94() set
S9 is set
S9 is Element of QC-symbols A
x. S9 is Element of bound_QC-variables A
[4,S9] is V15() set
{4,S9} is non empty finite V94() set
{{4,S9},{4}} is non empty finite V56() V94() set

proj1 S9 is set
S9 | { b1 where b1 is Element of QC-symbols A : x. b1 in proj2 S } is Relation-like Function-like set
proj2 (S9 | { b1 where b1 is Element of QC-symbols A : x. b1 in proj2 S } ) is set
S9 is set
proj1 (S9 | { b1 where b1 is Element of QC-symbols A : x. b1 in proj2 S } ) is set
l is set
(S9 | { b1 where b1 is Element of QC-symbols A : x. b1 in proj2 S } ) . l is set
S9 . l is set
l is Element of QC-symbols A

[4,l] is V15() set
{4,l} is non empty finite V94() set
{{4,l},{4}} is non empty finite V56() V94() set
s is Element of QC-symbols A

[4,s] is V15() set
{4,s} is non empty finite V94() set
{{4,s},{4}} is non empty finite V56() V94() set
S9 is set
l is set
S9 . S9 is set
S9 . l is set
l is Element of QC-symbols A

[4,l] is V15() set
{4,l} is non empty finite V94() set
{{4,l},{4}} is non empty finite V56() V94() set
s is Element of QC-symbols A

[4,s] is V15() set
{4,s} is non empty finite V94() set
{{4,s},{4}} is non empty finite V56() V94() set
proj1 (S9 | { b1 where b1 is Element of QC-symbols A : x. b1 in proj2 S } ) is set
S9 is Element of bool ()

proj1 (S9 | S9) is set
l is set
l is set
S9 /\ () is Element of bool ()
A is set
card A is V21() V22() V23() cardinal set
S is set
card S is V21() V22() V23() cardinal set
S \ A is Element of bool S
bool S is non empty set

QC-WFF A is non empty set
(A) is functional non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set
S is Element of QC-WFF A
(A,S) is finite V94() Element of bool ()
bool () is non empty set
(A,S) is finite V94() Element of bool
bool is non empty set
{ b1 where b1 is Element of QC-symbols A : x. b1 in (A,S) } is set
SQ is Relation-like Function-like finite V94() Element of (A)
(A,SQ) is finite V94() Element of bool ()
proj2 SQ is finite V94() set
{ b1 where b1 is Element of QC-symbols A : x. b1 in proj2 SQ } is set
(A,S) \/ (A,SQ) is finite V94() Element of bool ()
NAT \ ((A,S) \/ (A,SQ)) is V45() V46() V47() V48() V49() V50() Element of bool REAL
card ((A,S) \/ (A,SQ)) is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
card NAT is non empty non trivial V21() V22() V23() non finite cardinal set

(A) is functional non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set
QC-WFF A is non empty set
SQ is Element of QC-WFF A
S is Relation-like Function-like finite V94() Element of (A)
(A,SQ,S) is non empty Element of bool ()
bool () is non empty set
(A,SQ) is finite V94() Element of bool ()
(A,SQ) is finite V94() Element of bool
bool is non empty set
{ b1 where b1 is Element of QC-symbols A : x. b1 in (A,SQ) } is set
(A,S) is finite V94() Element of bool ()
proj2 S is finite V94() set
{ b1 where b1 is Element of QC-symbols A : x. b1 in proj2 S } is set
(A,SQ) \/ (A,S) is finite V94() Element of bool ()
NAT \ ((A,SQ) \/ (A,S)) is V45() V46() V47() V48() V49() V50() Element of bool REAL
the Element of (A,SQ,S) is Element of (A,SQ,S)

QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bound_QC-variables A is non empty Element of bool ()
bool () is non empty set
[:{4},():] is non empty set
QC-WFF A is non empty set
(A) is functional non empty set
PFuncs (,) is functional non empty set
S9 is Relation-like Function-like finite V94() Element of (A)

SQ is Element of QC-WFF A
All (S,SQ) is Element of QC-WFF A

1 + 1 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT

[:NAT,():] is non empty non trivial non finite set

proj2 S9 is finite V94() set
is non empty set
(A,S9,SQ) is Element of QC-symbols A
(A,SQ,S9) is non empty Element of bool ()
bool () is non empty set
(A,SQ) is finite V94() Element of bool ()
(A,SQ) is finite V94() Element of bool
bool is non empty set
{ b1 where b1 is Element of QC-symbols A : x. b1 in (A,SQ) } is set
(A,S9) is finite V94() Element of bool ()
{ b1 where b1 is Element of QC-symbols A : x. b1 in proj2 S9 } is set
(A,SQ) \/ (A,S9) is finite V94() Element of bool ()
NAT \ ((A,SQ) \/ (A,S9)) is V45() V46() V47() V48() V49() V50() Element of bool REAL
the Element of (A,SQ,S9) is Element of (A,SQ,S9)
x. (A,S9,SQ) is Element of bound_QC-variables A
[4,(A,S9,SQ)] is V15() set
{4,(A,S9,SQ)} is non empty finite V94() set
{{4,(A,S9,SQ)},{4}} is non empty finite V56() V94() set
[S,(x. (A,S9,SQ))] is V15() Element of
{S,(x. (A,S9,SQ))} is non empty finite V94() set
{S} is non empty trivial finite 1 -element V94() set
{{S,(x. (A,S9,SQ))},{S}} is non empty finite V56() V94() set

bool is non empty set
S9 \/ {[S,(x. (A,S9,SQ))]} is non empty finite V94() set
[S,S] is V15() Element of
{S,S} is non empty finite V94() set
{{S,S},{S}} is non empty finite V56() V94() set

S9 \/ {[S,S]} is non empty finite V94() set
l is Relation-like Function-like Element of (A)
(A,S,(All (S,SQ)),l) is Relation-like Function-like finite V94() Element of (A)
still_not-bound_in (All (S,SQ)) is Element of bool
proj1 l is set
{ b1 where b1 is Element of bound_QC-variables A : ( b1 in still_not-bound_in (All (S,SQ)) & b1 is Element of proj1 l & not b1 = S & not b1 = l . b1 ) } is set
(A,l, { b1 where b1 is Element of bound_QC-variables A : ( b1 in still_not-bound_in (All (S,SQ)) & b1 is Element of proj1 l & not b1 = S & not b1 = l . b1 ) } ) is Relation-like Function-like Element of (A)
l is Relation-like Function-like Element of (A)
(A,S,(All (S,SQ)),l) is Relation-like Function-like finite V94() Element of (A)
still_not-bound_in (All (S,SQ)) is Element of bool
proj1 l is set
{ b1 where b1 is Element of bound_QC-variables A : ( b1 in still_not-bound_in (All (S,SQ)) & b1 is Element of proj1 l & not b1 = S & not b1 = l . b1 ) } is set
(A,l, { b1 where b1 is Element of bound_QC-variables A : ( b1 in still_not-bound_in (All (S,SQ)) & b1 is Element of proj1 l & not b1 = S & not b1 = l . b1 ) } ) is Relation-like Function-like Element of (A)
proj1 S9 is finite V94() set
S9 is Relation-like set
proj1 S9 is set
(proj1 S9) /\ (proj1 S9) is finite V94() set
s is set
{S} is non empty trivial finite 1 -element V94() Element of bool
P9 is Element of bound_QC-variables A
l . P9 is set

dom (A,S9) is Element of bool

proj1 l is set
(dom (A,S9)) /\ () is Element of bool
l is set
(A,S9) . l is set
l . l is set
(A,S9) \/ l is set

l is Relation-like Function-like Element of (A)
(A,S,(All (S,SQ)),l) is Relation-like Function-like finite V94() Element of (A)
proj1 l is set
{ b1 where b1 is Element of bound_QC-variables A : ( b1 in still_not-bound_in (All (S,SQ)) & b1 is Element of proj1 l & not b1 = S & not b1 = l . b1 ) } is set
(A,l, { b1 where b1 is Element of bound_QC-variables A : ( b1 in still_not-bound_in (All (S,SQ)) & b1 is Element of proj1 l & not b1 = S & not b1 = l . b1 ) } ) is Relation-like Function-like Element of (A)
l is Relation-like Function-like Element of (A)
(A,S,(All (S,SQ)),l) is Relation-like Function-like finite V94() Element of (A)
proj1 l is set
{ b1 where b1 is Element of bound_QC-variables A : ( b1 in still_not-bound_in (All (S,SQ)) & b1 is Element of proj1 l & not b1 = S & not b1 = l . b1 ) } is set
(A,l, { b1 where b1 is Element of bound_QC-variables A : ( b1 in still_not-bound_in (All (S,SQ)) & b1 is Element of proj1 l & not b1 = S & not b1 = l . b1 ) } ) is Relation-like Function-like Element of (A)
S9 is Relation-like set
proj1 S9 is set
(proj1 S9) /\ (proj1 S9) is finite V94() set
s is set
P9 is Element of bound_QC-variables A
l . P9 is set

proj1 l is set
(dom (A,S9)) /\ () is Element of bool
l is set
(A,S9) . l is set
l . l is set
(A,S9) \/ l is set

QC-WFF A is non empty set
(A) is functional non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set

QC-WFF A is non empty set
(A) is functional non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set
S is set
SQ is set
S9 is set
S9 is Element of QC-WFF A
l is Relation-like Function-like Element of (A)
[S9,l] is V15() Element of [:(),(A):]
[:(),(A):] is non empty set
{S9,l} is non empty finite V94() set
{S9} is non empty trivial finite 1 -element V94() set
{{S9,l},{S9}} is non empty finite V56() V94() set
S9 is Element of QC-WFF A
l is Relation-like Function-like Element of (A)
[S9,l] is V15() Element of [:(),(A):]
[:(),(A):] is non empty set
{S9,l} is non empty finite V94() set
{S9} is non empty trivial finite 1 -element V94() set
{{S9,l},{S9}} is non empty finite V56() V94() set
l is Element of QC-WFF A
s is Relation-like Function-like Element of (A)
[l,s] is V15() Element of [:(),(A):]
{l,s} is non empty finite V94() set
{l} is non empty trivial finite 1 -element V94() set
{{l,s},{l}} is non empty finite V56() V94() set
l is Element of QC-WFF A
s is Relation-like Function-like Element of (A)
[l,s] is V15() Element of [:(),(A):]
{l,s} is non empty finite V94() set
{l} is non empty trivial finite 1 -element V94() set
{{l,s},{l}} is non empty finite V56() V94() set

the_scope_of S9 is Element of QC-WFF A
(A,(bound_in S9),S9,l) is Relation-like Function-like finite V94() Element of (A)

bool is non empty set
proj1 l is set
{ b1 where b1 is Element of bound_QC-variables A : ( b1 in still_not-bound_in S9 & b1 is Element of proj1 l & not b1 = bound_in S9 & not b1 = l . b1 ) } is set
(A,l, { b1 where b1 is Element of bound_QC-variables A : ( b1 in still_not-bound_in S9 & b1 is Element of proj1 l & not b1 = bound_in S9 & not b1 = l . b1 ) } ) is Relation-like Function-like Element of (A)
(A,(bound_in S9),(),(A,(bound_in S9),S9,l)) is Relation-like Function-like Element of (A)
[:(),(A):] is non empty set

SQ is set
S9 is set
S9 is set
[S9,S9] is V15() set
{S9,S9} is non empty finite V94() set
{S9} is non empty trivial finite 1 -element V94() set
{{S9,S9},{S9}} is non empty finite V56() V94() set
l is Element of QC-WFF A
l is Relation-like Function-like Element of (A)
[l,l] is V15() Element of [:(),(A):]
{l,l} is non empty finite V94() set
{l} is non empty trivial finite 1 -element V94() set
{{l,l},{l}} is non empty finite V56() V94() set
S9 is Element of QC-WFF A
S9 is Relation-like Function-like Element of (A)
[S9,S9] is V15() Element of [:(),(A):]
{S9,S9} is non empty finite V94() set
{S9} is non empty trivial finite 1 -element V94() set
{{S9,S9},{S9}} is non empty finite V56() V94() set
l is set
[[S9,S9],l] is V15() set
{[S9,S9],l} is non empty finite V94() set
{[S9,S9]} is Function-like non empty trivial finite 1 -element V94() set
{{[S9,S9],l},{[S9,S9]}} is non empty finite V56() V94() set
SQ is set
S9 is set
S9 is Element of QC-WFF A
l is Relation-like Function-like Element of (A)
[S9,l] is V15() Element of [:(),(A):]
{S9,l} is non empty finite V94() set
{S9} is non empty trivial finite 1 -element V94() set
{{S9,l},{S9}} is non empty finite V56() V94() set
l is set
[[S9,l],l] is V15() set
{[S9,l],l} is non empty finite V94() set

{{[S9,l],l},{[S9,l]}} is non empty finite V56() V94() set

S9 is set
S9 is Element of QC-WFF A
l is Relation-like Function-like Element of (A)
[S9,l] is V15() Element of [:(),(A):]
[:(),(A):] is non empty set
{S9,l} is non empty finite V94() set
{S9} is non empty trivial finite 1 -element V94() set
{{S9,l},{S9}} is non empty finite V56() V94() set
l is set
[[S9,l],l] is V15() set
{[S9,l],l} is non empty finite V94() set

{{[S9,l],l},{[S9,l]}} is non empty finite V56() V94() set
S9 is Element of QC-WFF A
l is Relation-like Function-like Element of (A)
[S9,l] is V15() Element of [:(),(A):]
[:(),(A):] is non empty set
{S9,l} is non empty finite V94() set
{S9} is non empty trivial finite 1 -element V94() set
{{S9,l},{S9}} is non empty finite V56() V94() set
l is set
[[S9,l],l] is V15() set
{[S9,l],l} is non empty finite V94() set

{{[S9,l],l},{[S9,l]}} is non empty finite V56() V94() set
is non empty non trivial non finite set
is non empty non trivial non finite set
bool is non empty non trivial non finite set
[0,0] is V15() Element of

[1,0] is V15() Element of

[2,0] is V15() Element of

[3,0] is V15() Element of

QC-WFF A is non empty set
(A) is functional non empty set
bound_QC-variables A is non empty Element of bool ()
QC-variables A is non empty set
QC-symbols A is non empty set
proj2 A is set
[:{4,5},():] is non empty set
\/ [:{4,5},():] is non empty set
bool () is non empty set
[:{4},():] is non empty set
PFuncs (,) is functional non empty set
[:(),(A):] is non empty set
[:NAT,():] is non empty non trivial non finite set

[:([:NAT,():] *),(A):] is non empty set
bool [:([:NAT,():] *),(A):] is non empty set
QC-pred_symbols A is non empty set
7 is non empty ext-real positive non negative V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
{ [b1,b2] where b1 is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT , b2 is Element of QC-symbols A : 7 <= b1 } is set
[:NAT,[:NAT,():]:] is non empty non trivial non finite set
bool [:NAT,[:NAT,():]:] is non empty non trivial non finite set

bool ([:NAT,():] *) is non empty set
S is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
S -ary_QC-pred_symbols A is non empty Element of bool ()
bool () is non empty set
{ b1 where b1 is Element of QC-pred_symbols A : the_arity_of b1 = S } is set
SQ is Element of S -ary_QC-pred_symbols A

1 + S is ext-real V21() V22() V23() V27() V28() V32() V43() V44() V45() V46() V47() V48() V49() V50() finite cardinal V94() Element of NAT
S9 is Relation-like Function-like Element of (A)
[(<*SQ*> ^ S9),S9] is V15() set
{(<*SQ*> ^ S9),S9} is functional non empty finite V94() set
{(<*SQ*> ^ S9)} is functional non empty trivial finite V56() 1 -element V92() V94() set
{{(<*SQ*> ^ S9),S9},{(<*SQ*> ^ S9)}} is non empty finite V56() V94() set
SQ ! S9 is Element of QC-WFF A
VERUM A is Element of CQC-WFF A
CQC-WFF A is non empty Element of bool ()
bool () is non empty set
S is Relation-like Function-like Element of (A)
[,S] is V15() Element of [:,(A):]
[:,(A):] is non empty non trivial non finite set
{,S} is functional non empty finite V94() set

is non empty finite V56() V94() set

SQ is Relation-like Function-like Element of (A)
[S,SQ] is V15() Element of [:(),(A):]
[:(),(A):] is non empty non trivial non finite set
{S,SQ} is functional non empty finite V94() set
{S} is functional non empty trivial finite V56() 1 -element V92() V94() set
{{S,SQ},{S}} is non empty finite V56() V94() set
[(<*[1,0]*> ^ S),SQ] is V15() set
{(<*[1,0]*> ^ S),SQ} is functional non empty finite V94() set
{(<*[1,0]*> ^ S)} is functional non empty trivial finite V56() 1 -element V92() V94() set
{{(<*[1,0]*> ^ S),SQ},{(<*[1,0]*> ^ S)}} is non empty finite V56() V94() set
S9 is set
l is set
[S9,l] is V15() set
{S9,l} is non empty finite V94() set
{S9} is non empty trivial finite 1 -element V94() set
{{S9,l},{S9}} is non empty finite V56() V94() set
S9 is Element of QC-WFF A
'not' S9 is Element of QC-WFF A

S9 is Relation-like Function-like Element of (A)
[S,S9] is V15() Element of [:(),(A):]
[:(),(A):] is non empty non trivial non finite set
{S,S9} is functional non empty finite V94() set
{S} is functional non empty trivial finite V56() 1 -element V92() V94() set
{{S,S9},{S}} is non empty finite V56() V94() set
[SQ,S9] is V15() Element of [:(),(A):]
{SQ,S9} is functional non empty finite V94() set
{SQ} is functional non empty trivial finite V56() 1 -element V92() V94() set
{{SQ,S9},{SQ}} is non empty finite V56() V94() set
[((<*[2,0]*> ^ S) ^ SQ),S9] is V15() set
{((<*[2,0]*> ^ S) ^ SQ),S9} is functional non empty finite V94() set
{((<*[2,0]*> ^ S) ^ SQ)} is functional non empty trivial finite V56() 1 -element V92() V94() set
{{((<*[2,0]*> ^ S) ^ SQ),S9},{((<*[2,0]*> ^ S) ^ SQ)}} is non empty finite V56() V94() set
l is set
l is set
[l,l] is V15() set
{l,l} is non empty finite V94() set
{l} is non empty trivial finite 1 -element V94() set
{{l,l},{l}} is non empty finite V56() V94() set
l is set
s is set
[l,s] is V15() set
{l,s} is non empty finite V94() set
{l} is non empty trivial finite 1 -element V94() set
{{l,s},{l}