:: AFINSQ_1 semantic presentation

REAL is non empty non trivial non finite V66() V67() V68() V72() V80() V81() V83() set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal V66() V67() V68() V69() V70() V71() V72() V78() V80() Element of bool REAL
bool REAL is non empty non trivial non finite set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal V66() V67() V68() V69() V70() V71() V72() V78() V80() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V66() V72() set
RAT is non empty non trivial non finite V66() V67() V68() V69() V72() set
INT is non empty non trivial non finite V66() V67() V68() V69() V70() V72() set
K360(NAT) is V90() set
{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() set
the Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() set is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() set
1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() Element of NAT
{{}} is functional non empty trivial finite V44() 1 -element V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
{{},1} is non empty finite V44() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
K313({},1,2) is non empty finite V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
4 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
K314({},1,2,3) is non empty finite set
5 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
K315({},1,2,3,4) is non empty finite set
6 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
K316({},1,2,3,4,5) is non empty finite set
7 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
K317({},1,2,3,4,5,6) is non empty finite set
8 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
K318({},1,2,3,4,5,6,7) is non empty finite set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 /\ x2 is finite set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
{x1} is non empty trivial finite V44() 1 -element V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
x1 \/ {x1} is non empty finite set
x1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
succ x1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
Seg x1 is finite x1 -element V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x2 is set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
{0} is functional non empty trivial finite V44() 1 -element V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
Seg x1 is finite x1 -element V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
{0} \/ (Seg x1) is non empty finite V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
x2 is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT : not x1 + 1 <= b₁ } is set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x3 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 is Relation-like Function-like set
dom x1 is set
x2 is Relation-like Function-like set
dom x2 is set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is Relation-like T-Sequence-like Function-like finite set
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is Relation-like T-Sequence-like Function-like finite set
card x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
card (dom x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like T-Sequence-like Function-like finite set
card x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
card x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like T-Sequence-like Function-like finite set
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT : not (x1) <= b₁ } is set
x2 is set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like Function-like set
dom x1 is set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is Relation-like Function-like set
dom x3 is set
x4 is Relation-like T-Sequence-like Function-like finite set
m is set
l is set
[m,l] is set
{m,l} is non empty finite set
{m} is non empty trivial finite 1 -element set
{{m,l},{m}} is non empty finite V44() set
x4 . m is set
[m,(x4 . m)] is set
{m,(x4 . m)} is non empty finite set
{{m,(x4 . m)},{m}} is non empty finite V44() set
x1 . m is set
F₁() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT : not F₁() <= b₁ } is set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like Function-like set
dom x1 is set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 . x3 is set
F₁() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is Relation-like Function-like set
dom x1 is set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 . x3 is set
F₂(x3) is set
x1 is set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x3 is set
x4 is set
[x3,x4] is set
{x3,x4} is non empty finite set
{x3} is non empty trivial finite 1 -element set
{{x3,x4},{x3}} is non empty finite V44() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x2 . m is set
[m,(x2 . m)] is set
{m,(x2 . m)} is non empty finite set
{m} is non empty trivial finite V44() 1 -element V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
{{m,(x2 . m)},{m}} is non empty finite V44() set
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x3 is set
x1 . x3 is set
x2 . x3 is set
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 . x3 is set
x2 . x3 is set
x1 is Relation-like T-Sequence-like Function-like finite set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 | x2 is Relation-like rng x1 -valued T-Sequence-like Function-like finite set
rng x1 is finite set
x1 is Relation-like Function-like set
dom x1 is set
x2 is Relation-like T-Sequence-like Function-like finite set
rng x2 is finite set
x2 (#) x1 is Relation-like Function-like finite set
dom (x2 (#) x1) is finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 | x1 is Relation-like rng x2 -valued T-Sequence-like Function-like finite set
rng x2 is finite set
((x2 | x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is set
x1 is set
[:NAT,x1:] is Relation-like set
bool [:NAT,x1:] is non empty set
x2 is Relation-like x1 -valued T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
rng x2 is finite set
x1 is Relation-like Function-like set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is set
x1 --> x2 is Relation-like x1 -defined T-Sequence-like Function-like constant total V25(x1,{x2}) finite Element of bool [:x1,{x2}:]
{x2} is non empty trivial finite 1 -element set
[:x1,{x2}:] is Relation-like finite set
bool [:x1,{x2}:] is non empty finite V44() set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is non empty set
the Element of x2 is Element of x2
x1 --> the Element of x2 is Relation-like x1 -defined x2 -valued T-Sequence-like Function-like constant total V25(x1,x2) finite Element of bool [:x1,x2:]
[:x1,x2:] is Relation-like set
bool [:x1,x2:] is non empty set
{ the Element of x2} is non empty trivial finite 1 -element set
[:x1,{ the Element of x2}:] is Relation-like finite set
m is Relation-like T-Sequence-like Function-like finite set
l is Relation-like x2 -valued T-Sequence-like Function-like finite set
(l) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is set
rng {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial ext-real non positive non negative V34() Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() set
x1 is set
x1 is non empty set
x3 is Relation-like x1 -valued T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
x1 is set
(x1) is set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
x1 is set
x1 is set
(x1) is Relation-like x1 -valued T-Sequence-like Function-like finite set
x1 is Relation-like T-Sequence-like Function-like finite set
x2 is Relation-like T-Sequence-like Function-like finite set
x1 ^ x2 is Relation-like T-Sequence-like Function-like set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) + (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x3 is Relation-like T-Sequence-like Function-like set
dom x3 is epsilon-transitive epsilon-connected ordinal set
(x1) +^ (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 . x4 is set
x1 . x4 is set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) +^ x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 . ((x1) +^ x4) is set
x2 . x4 is set
(x1) + x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x3 . ((x1) + x4) is set
x4 is epsilon-transitive epsilon-connected ordinal set
(x1) +^ x4 is epsilon-transitive epsilon-connected ordinal set
x3 . ((x1) +^ x4) is set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x1) + m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x3 . ((x1) + m) is set
x2 . x4 is set
x4 is epsilon-transitive epsilon-connected ordinal set
x3 . x4 is set
x1 . x4 is set
x1 is Relation-like T-Sequence-like Function-like finite set
x2 is Relation-like T-Sequence-like Function-like finite set
x1 ^ x2 is Relation-like T-Sequence-like Function-like set
dom (x1 ^ x2) is epsilon-transitive epsilon-connected ordinal set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x1) +^ (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is Relation-like T-Sequence-like Function-like finite set
x2 is Relation-like T-Sequence-like Function-like finite set
x1 ^ x2 is Relation-like T-Sequence-like Function-like finite set
((x1 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1 ^ x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) + (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 - (x2) is ext-real V52() V55() set
x3 is Relation-like T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) + (x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x2 ^ x3 is Relation-like T-Sequence-like Function-like finite set
(x2 ^ x3) . x1 is set
x3 . (x1 - (x2)) is set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) + x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x2) + (x3)) - (x2) is ext-real V52() V55() set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 - (x2) is ext-real V52() V55() set
x3 is Relation-like T-Sequence-like Function-like finite set
x2 ^ x3 is Relation-like T-Sequence-like Function-like finite set
((x2 ^ x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x2 ^ x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2 ^ x3) . x1 is set
x3 . (x1 - (x2)) is set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) + (x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is Relation-like T-Sequence-like Function-like finite set
x2 ^ x3 is Relation-like T-Sequence-like Function-like finite set
((x2 ^ x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) + (x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) + x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x3) + (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x3) + (x2)) - (x2) is ext-real V52() V55() set
x4 + (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x4 + (x2)) - (x2) is ext-real V52() V55() set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) + x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like T-Sequence-like Function-like set
dom x1 is epsilon-transitive epsilon-connected ordinal set
x2 is Relation-like T-Sequence-like Function-like set
x1 ^ x2 is Relation-like T-Sequence-like Function-like set
dom (x1 ^ x2) is epsilon-transitive epsilon-connected ordinal set
dom x2 is epsilon-transitive epsilon-connected ordinal set
(dom x1) +^ (dom x2) is epsilon-transitive epsilon-connected ordinal set
x1 is set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x3 is Relation-like T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 ^ x2 is Relation-like T-Sequence-like Function-like finite set
((x3 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x3) + x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) + (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x3 is Relation-like T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) + x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x3 ^ x2 is Relation-like T-Sequence-like Function-like finite set
((x3 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) + x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like T-Sequence-like Function-like finite set
rng x1 is finite set
x2 is Relation-like T-Sequence-like Function-like finite set
x1 ^ x2 is Relation-like T-Sequence-like Function-like finite set
rng (x1 ^ x2) is finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x1 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x3 is set
x4 is set
x1 . x4 is set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x1 ^ x2) . m is set
x1 . m is set
x1 is Relation-like T-Sequence-like Function-like finite set
rng x1 is finite set
x2 is Relation-like T-Sequence-like Function-like finite set
x2 ^ x1 is Relation-like T-Sequence-like Function-like finite set
rng (x2 ^ x1) is finite set
x3 is set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x4 is set
x1 . x4 is set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x2) + m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x2 ^ x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x2 ^ x1) . ((x2) + m) is set
x1 . m is set
x1 is Relation-like T-Sequence-like Function-like finite set
rng x1 is finite set
x2 is Relation-like T-Sequence-like Function-like finite set
x1 ^ x2 is Relation-like T-Sequence-like Function-like finite set
rng (x1 ^ x2) is finite set
rng x2 is finite set
(rng x1) \/ (rng x2) is finite set
x3 is set
((x1 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x4 is set
(x1 ^ x2) . x4 is set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) + (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) + l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x1) + (x2)) - (x1) is ext-real V52() V55() set
l + (x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(l + (x1)) - (x1) is ext-real V52() V55() set
m - (x1) is ext-real V52() V55() set
x2 . (m - (x1)) is set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 . m is set
x1 is Relation-like T-Sequence-like Function-like finite set
x2 is Relation-like T-Sequence-like Function-like finite set
x1 ^ x2 is Relation-like T-Sequence-like Function-like finite set
x3 is Relation-like T-Sequence-like Function-like finite set
(x1 ^ x2) ^ x3 is Relation-like T-Sequence-like Function-like finite set
x2 ^ x3 is Relation-like T-Sequence-like Function-like finite set
x1 ^ (x2 ^ x3) is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((x1 ^ x2) ^ x3) . x4 is set
x1 . x4 is set
((x1 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x1 ^ x2) . x4 is set
((x2 ^ x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) + x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x1 ^ x2) ^ x3) . ((x1) + x4) is set
(x2 ^ x3) . x4 is set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) + m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x1) + (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x1) + (x2)) + m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x1 ^ x2) ^ x3) . (((x1) + (x2)) + m) is set
((x1 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1 ^ x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((x1 ^ x2)) + m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x1 ^ x2) ^ x3) . (((x1 ^ x2)) + m) is set
x3 . m is set
((x1 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x1 ^ x2) . ((x1) + x4) is set
x2 . x4 is set
(((x1 ^ x2) ^ x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x1 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1 ^ x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((x1 ^ x2)) + (x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) + (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x1) + (x2)) + (x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x2) + (x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x1) + ((x2) + (x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x2 ^ x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x2 ^ x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) + ((x2 ^ x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like T-Sequence-like Function-like finite set
x2 is Relation-like T-Sequence-like Function-like finite set
x1 ^ x2 is Relation-like T-Sequence-like Function-like finite set
x2 ^ x1 is Relation-like T-Sequence-like Function-like finite set
x3 is Relation-like T-Sequence-like Function-like finite set
x3 ^ x2 is Relation-like T-Sequence-like Function-like finite set
x2 ^ x3 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) + (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x3 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x3 ^ x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) + (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 . x4 is set
x3 . x4 is set
(x3 ^ x2) . x4 is set
(x2) + (x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x2 ^ x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x2 ^ x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) + (x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 . x4 is set
x3 . x4 is set
(x2) + x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x2 ^ x3) . ((x2) + x4) is set
x1 is Relation-like T-Sequence-like Function-like finite set
x1 ^ {} is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 . x2 is set
(x1 ^ {}) . x2 is set
((x1 ^ {})) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
({}) is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() Element of NAT
dom {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() set
(x1) + ({}) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
{} ^ x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 . x2 is set
({} ^ x1) . x2 is set
({}) is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() Element of NAT
dom {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() set
({}) + x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
({} ^ x1) . (({}) + x2) is set
(({} ^ x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
({}) is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() Element of NAT
dom {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
({}) + (x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like T-Sequence-like Function-like finite set
x2 is Relation-like T-Sequence-like Function-like finite set
x1 ^ x2 is Relation-like T-Sequence-like Function-like finite set
((x1 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1 ^ x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) + (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is set
x2 is Relation-like x1 -valued T-Sequence-like Function-like finite set
x3 is Relation-like x1 -valued T-Sequence-like Function-like finite set
x2 ^ x3 is Relation-like T-Sequence-like Function-like finite set
rng x3 is finite set
rng (x2 ^ x3) is finite set
rng x2 is finite set
(rng x2) \/ (rng x3) is finite set
x1 is set
x2 is set
[x1,x2] is set
{x1,x2} is non empty finite set
{x1} is non empty trivial finite 1 -element set
{{x1,x2},{x1}} is non empty finite V44() set
x3 is set
x4 is set
[x3,x4] is set
{x3,x4} is non empty finite set
{x3} is non empty trivial finite 1 -element set
{{x3,x4},{x3}} is non empty finite V44() set
{[x3,x4]} is Relation-like Function-like constant non empty trivial finite 1 -element set
x1 is set
(x1) is non empty set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
x2 is Relation-like Function-like set
dom x2 is set
x2 . 0 is set
[0,(x2 . 0)] is set
{0,(x2 . 0)} is non empty finite set
{{0,(x2 . 0)},{0}} is non empty finite V44() set
{[0,(x2 . 0)]} is Relation-like Function-like constant non empty trivial finite 1 -element set
x3 is Relation-like Function-like set
x4 is set
m is set
[x4,m] is set
{x4,m} is non empty finite set
{x4} is non empty trivial finite 1 -element set
{{x4,m},{x4}} is non empty finite V44() set
rng x2 is set
{(x2 . 0)} is non empty trivial finite 1 -element set
x1 is set
(x1) is Relation-like Function-like non empty set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
x1 is set
(x1) is Relation-like Function-like non empty set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
dom (x1) is non empty set
x1 is Relation-like T-Sequence-like Function-like finite set
x2 is Relation-like T-Sequence-like Function-like finite set
x1 ^ x2 is Relation-like T-Sequence-like Function-like finite set
x3 is set
rng (x1 ^ x2) is finite set
rng x1 is finite set
rng x2 is finite set
(rng x1) \/ (rng x2) is finite set
x1 is set
(x1) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
x2 is set
(x2) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like T-Sequence-like Function-like finite set
x3 is set
(x3) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
((x1) ^ (x2)) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
x1 is set
x2 is set
(x1,x2) is set
(x1) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
(x2) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like T-Sequence-like Function-like finite set
x3 is set
(x1,x2,x3) is set
(x3) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
((x1) ^ (x2)) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
x1 is set
x2 is set
(x1,x2) is Relation-like Function-like set
(x1) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
(x2) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like T-Sequence-like Function-like finite set
x3 is set
(x1,x2,x3) is Relation-like Function-like set
(x3) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
((x1) ^ (x2)) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
x1 is set
(x1) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
[0,x1] is set
{0,x1} is non empty finite set
{{0,x1},{0}} is non empty finite V44() set
{[0,x1]} is Relation-like Function-like constant non empty trivial finite 1 -element set
x1 is set
(x1) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
rng x2 is finite set
x2 . 0 is set
{(x2 . 0)} is non empty trivial finite 1 -element set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x2 . 0 is set
x2 is Relation-like T-Sequence-like Function-like finite set
x1 is set
(x1) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 . 0 is set
x4 is Relation-like T-Sequence-like Function-like finite set
(x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 . 0 is set
x3 is set
(x3) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
x1 is set
(x1) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x1) ^ x2 is Relation-like T-Sequence-like Function-like finite set
((x1) ^ x2) . 0 is set
((x1)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
(x1) . 0 is set
x1 is set
(x1) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
x2 is Relation-like T-Sequence-like Function-like finite set
x2 ^ (x1) is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2 ^ (x1)) . (x2) is set
((x1)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(x2) + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x1) . 0 is set
x1 is set
x2 is set
x3 is set
(x1,x2,x3) is Relation-like T-Sequence-like Function-like finite set
(x1) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
(x2) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like T-Sequence-like Function-like finite set
(x3) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
((x1) ^ (x2)) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
(x2,x3) is Relation-like T-Sequence-like Function-like finite set
(x2) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
(x1) ^ (x2,x3) is Relation-like T-Sequence-like Function-like finite set
x4 is set
m is set
l is set
(x4,m,l) is Relation-like T-Sequence-like Function-like finite set
(x4) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x4 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
(m) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> m is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> m is Relation-like {0} -defined Function-like constant non empty total V25({0},{m}) finite Element of bool [:{0},{m}:]
{m} is non empty trivial finite 1 -element set
[:{0},{m}:] is Relation-like non empty finite set
bool [:{0},{m}:] is non empty finite V44() set
(x4) ^ (m) is Relation-like T-Sequence-like Function-like finite set
(l) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> l is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> l is Relation-like {0} -defined Function-like constant non empty total V25({0},{l}) finite Element of bool [:{0},{l}:]
{l} is non empty trivial finite 1 -element set
[:{0},{l}:] is Relation-like non empty finite set
bool [:{0},{l}:] is non empty finite V44() set
((x4) ^ (m)) ^ (l) is Relation-like T-Sequence-like Function-like finite set
(x4,m) is Relation-like T-Sequence-like Function-like finite set
(x4,m) ^ (l) is Relation-like T-Sequence-like Function-like finite set
x1 is set
x2 is set
(x1,x2) is Relation-like T-Sequence-like Function-like finite set
(x1) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
(x2) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like T-Sequence-like Function-like finite set
x3 is Relation-like T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 . 0 is set
x3 . 1 is set
((x1)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (x1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() set
((x2)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (x2) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() set
((x1)) + ((x2)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
1 + ((x2)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
((x2)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
((x1)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
(x1) . 0 is set
((x1)) + 0 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
((x1) ^ (x2)) . (((x1)) + 0) is set
(x2) . 0 is set
((x2)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
((x1)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (x1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((x1)) + x4 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x3 . (((x1)) + x4) is set
(x2) . x4 is set
1 + x4 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x3 . (1 + x4) is set
1 + 0 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x3 . (1 + 0) is set
(x2) . 0 is set
((x1)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 . x4 is set
(x1) . x4 is set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
((x1)) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
((x2)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (x2) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() set
((x1)) + ((x2)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 is set
x2 is set
x3 is set
(x1,x2,x3) is Relation-like T-Sequence-like Function-like finite set
(x1) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
(x2) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like T-Sequence-like Function-like finite set
(x3) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
((x1) ^ (x2)) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
x4 is Relation-like T-Sequence-like Function-like finite set
(x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 . 0 is set
x4 . 1 is set
x4 . 2 is set
((x1)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
((x3)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
(x1,x2) is Relation-like T-Sequence-like Function-like finite set
((x1,x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1,x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((x3)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (x3) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() set
((x1,x2)) + ((x3)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
2 + ((x3)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
2 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(x2,x3) is Relation-like T-Sequence-like Function-like finite set
(x2) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
(x1) ^ (x2,x3) is Relation-like T-Sequence-like Function-like finite set
((x1) ^ (x2,x3)) . 0 is set
(x1) . 0 is set
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(x1,x2) . 1 is set
(x1,x2) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
((x1,x2)) + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x1,x2) ^ (x3)) . (((x1,x2)) + 0) is set
(x3) . 0 is set
(x1,x2) is Relation-like T-Sequence-like Function-like finite set
((x1,x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x1,x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1,x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 . m is set
(x1,x2) . m is set
((x3)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
((x1,x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1,x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((x1,x2)) + m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 . (((x1,x2)) + m) is set
(x3) . m is set
2 + 0 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x4 . (2 + 0) is set
(x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
2 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
((x1,x2)) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
((x3)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (x3) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() set
((x1,x2)) + ((x3)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 is set
(x1) is Relation-like T-Sequence-like Function-like non empty finite set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
card (x1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (x1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() set
x2 is set
(x1,x2) is Relation-like T-Sequence-like Function-like finite set
(x2) is Relation-like T-Sequence-like Function-like constant non empty trivial finite 1 -element set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like T-Sequence-like Function-like finite set
card (x1,x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1,x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is set
(x1,x2,x3) is Relation-like T-Sequence-like Function-like finite set
(x3) is Relation-like T-Sequence-like Function-like constant non empty trivial finite 1 -element set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
((x1) ^ (x2)) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
card (x1,x2,x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1,x2,x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
card x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is set
x1 --> x2 is Relation-like x1 -defined T-Sequence-like Function-like constant total V25(x1,{x2}) finite Element of bool [:x1,{x2}:]
{x2} is non empty trivial finite 1 -element set
[:x1,{x2}:] is Relation-like finite set
bool [:x1,{x2}:] is non empty finite V44() set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 --> 0 is Relation-like x1 -defined NAT -valued T-Sequence-like Function-like constant total V25(x1, NAT ) Ordinal-yielding Function-yielding V39() finite Element of bool [:x1,NAT:]
[:x1,NAT:] is Relation-like set
bool [:x1,NAT:] is non empty set
[:x1,{0}:] is Relation-like finite set
card (x1 --> 0) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1 --> 0) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like x1 -defined T-Sequence-like Function-like finite x1 -element set
card x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal x1 -element V52() V55() set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal x1 -element V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 | x3 is Relation-like rng x1 -valued T-Sequence-like Function-like finite set
rng x1 is finite set
((x1 | x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x1) /\ x3 is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x1) - 1 is ext-real V52() V55() set
x1 . ((x1) - 1) is set
((x1 . ((x1) - 1))) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> (x1 . ((x1) - 1)) is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> (x1 . ((x1) - 1)) is Relation-like {0} -defined Function-like constant non empty total V25({0},{(x1 . ((x1) - 1))}) finite Element of bool [:{0},{(x1 . ((x1) - 1))}:]
{(x1 . ((x1) - 1))} is non empty trivial finite 1 -element set
[:{0},{(x1 . ((x1) - 1))}:] is Relation-like non empty finite set
bool [:{0},{(x1 . ((x1) - 1))}:] is non empty finite V44() set
(x1 | x3) ^ ((x1 . ((x1) - 1))) is Relation-like T-Sequence-like Function-like finite set
m is set
x1 . m is set
((x1 | x3) ^ ((x1 . ((x1) - 1)))) . m is set
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 . l is set
(x1 | x3) . l is set
((x1 | x3) ^ ((x1 . ((x1) - 1)))) . l is set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(((x1 . ((x1) - 1)))) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
{x3} is non empty trivial finite V44() 1 -element V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
((x1 | x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1 | x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((x1 | x3)) + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x1 | x3) ^ ((x1 . ((x1) - 1)))) . (((x1 | x3)) + 0) is set
((x1 . ((x1) - 1))) . 0 is set
x1 . x3 is set
x3 \/ {x3} is non empty finite V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
(((x1 | x3) ^ ((x1 . ((x1) - 1))))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x1 | x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1 | x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(((x1 . ((x1) - 1)))) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom ((x1 . ((x1) - 1))) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() set
((x1 | x3)) + (((x1 . ((x1) - 1)))) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 is non empty set
x2 is Element of x1
(x2) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x2 is Relation-like NAT -defined {0} -defined x1 -valued Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined x1 -valued Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
x3 is Element of x1
(x2,x3) is Relation-like 2 -defined T-Sequence-like Function-like total finite 2 -element set
(x3) is Relation-like 1 -defined x1 -valued T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x3 is Relation-like NAT -defined {0} -defined x1 -valued Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined x1 -valued Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
(x2) ^ (x3) is Relation-like x1 -valued T-Sequence-like Function-like finite set
x4 is Element of x1
(x2,x3,x4) is Relation-like 3 -defined T-Sequence-like Function-like total finite 3 -element set
(x4) is Relation-like 1 -defined x1 -valued T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x4 is Relation-like NAT -defined {0} -defined x1 -valued Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined x1 -valued Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
((x2) ^ (x3)) ^ (x4) is Relation-like x1 -valued T-Sequence-like Function-like finite set
x1 is Relation-like T-Sequence-like Function-like finite set
x2 is V66() V67() V68() Element of bool REAL
x3 is Relation-like T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x4 is Relation-like T-Sequence-like Function-like finite set
(x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
m is Relation-like T-Sequence-like Function-like finite set
l is set
(l) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> l is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> l is Relation-like {0} -defined Function-like constant non empty total V25({0},{l}) finite Element of bool [:{0},{l}:]
{l} is non empty trivial finite 1 -element set
[:{0},{l}:] is Relation-like non empty finite set
bool [:{0},{l}:] is non empty finite V44() set
m ^ (l) is Relation-like T-Sequence-like Function-like finite set
(m) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((l)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (l) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() set
(m) + ((l)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(m) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is set
(x2) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
x1 ^ (x2) is Relation-like T-Sequence-like Function-like finite set
((x1 ^ (x2))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1 ^ (x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is Relation-like T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 is Relation-like T-Sequence-like Function-like finite set
x3 ^ x4 is Relation-like T-Sequence-like Function-like finite set
m is Relation-like T-Sequence-like Function-like finite set
(x1 ^ (x2)) ^ m is Relation-like T-Sequence-like Function-like finite set
((x2)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (x2) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() set
(x1) + ((x2)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(x1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(x2) ^ m is Relation-like T-Sequence-like Function-like finite set
x1 ^ ((x2) ^ m) is Relation-like T-Sequence-like Function-like finite set
l is Relation-like T-Sequence-like Function-like finite set
x3 ^ l is Relation-like T-Sequence-like Function-like finite set
l ^ (x2) is Relation-like T-Sequence-like Function-like finite set
x3 ^ (l ^ (x2)) is Relation-like T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 . l is set
(x1 ^ (x2)) . l is set
((x1 ^ (x2)) ^ m) . l is set
x3 ^ {} is Relation-like T-Sequence-like Function-like finite set
l is Relation-like T-Sequence-like Function-like finite set
x3 ^ l is Relation-like T-Sequence-like Function-like finite set
R is Relation-like T-Sequence-like Function-like finite set
x3 ^ R is Relation-like T-Sequence-like Function-like finite set
({}) is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() Element of NAT
dom {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() set
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
x1 ^ x2 is Relation-like T-Sequence-like Function-like finite set
x3 is Relation-like T-Sequence-like Function-like finite set
{} ^ x3 is Relation-like T-Sequence-like Function-like finite set
x1 ^ {} is Relation-like T-Sequence-like Function-like finite set
x1 is Relation-like T-Sequence-like Function-like finite set
x2 is Relation-like T-Sequence-like Function-like finite set
x1 ^ x2 is Relation-like T-Sequence-like Function-like finite set
x3 is Relation-like T-Sequence-like Function-like finite set
x4 is Relation-like T-Sequence-like Function-like finite set
x3 ^ x4 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is set
[:NAT,x1:] is Relation-like set
bool [:NAT,x1:] is non empty set
x2 is set
x3 is set
x4 is Relation-like x1 -valued T-Sequence-like Function-like finite set
m is Relation-like Function-like Element of bool [:NAT,x1:]
x1 is set
(x1) is set
the Relation-like x1 -valued T-Sequence-like Function-like finite set is Relation-like x1 -valued T-Sequence-like Function-like finite set
x1 is set
x2 is set
(x2) is non empty set
x3 is set
x4 is set
(x4) is non empty set
x1 is set
(x1) is non empty set
(x1) is Relation-like non-empty empty-yielding NAT -defined x1 -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() set
F₁() is non empty set
(F₁()) is non empty set
x1 is set
x2 is set
x3 is Relation-like T-Sequence-like Function-like finite set
x2 is set
x4 is Relation-like T-Sequence-like Function-like finite set
x3 is set
x1 is Relation-like T-Sequence-like Function-like finite set
x2 is set
x3 is set
x1 +* (x2,x3) is Relation-like Function-like set
dom (x1 +* (x2,x3)) is set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x3 is set
x1 +* (x2,x3) is Relation-like T-Sequence-like Function-like finite set
((x1 +* (x2,x3))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1 +* (x2,x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1 +* (x2,x3)) . x2 is set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x1 +* (x2,x3)) . m is set
x1 . m is set
x1 is non empty set
x2 is Relation-like x1 -valued T-Sequence-like Function-like finite set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 is Element of x1
x2 +* (x3,x4) is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x3 .--> x4 is Relation-like NAT -defined {x3} -defined x1 -valued Function-like one-to-one finite set
{x3} is non empty trivial finite V44() 1 -element V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
{x3} --> x4 is Relation-like {x3} -defined x1 -valued Function-like constant non empty total V25({x3},{x4}) finite Element of bool [:{x3},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{x3},{x4}:] is Relation-like non empty finite set
bool [:{x3},{x4}:] is non empty finite V44() set
x2 +* (x3 .--> x4) is Relation-like Function-like finite set
rng (x2 +* (x3,x4)) is finite set
rng x2 is finite set
rng (x3 .--> x4) is finite set
(rng x2) \/ (rng (x3 .--> x4)) is finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
rng (x2 +* (x3,x4)) is finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is Relation-like REAL -valued T-Sequence-like Function-like finite set
rng x1 is finite set
x1 is Relation-like NAT -valued T-Sequence-like Function-like Ordinal-yielding finite set
rng x1 is finite set
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 . 0 is set
x1 . 1 is set
x1 . 2 is set
x1 . 3 is set
x2 is set
(x2) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
x3 is set
(x3) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
(x2) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
x4 is set
(x4) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x4 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
((x2) ^ (x3)) ^ (x4) is Relation-like T-Sequence-like Function-like finite set
m is set
(m) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> m is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> m is Relation-like {0} -defined Function-like constant non empty total V25({0},{m}) finite Element of bool [:{0},{m}:]
{m} is non empty trivial finite 1 -element set
[:{0},{m}:] is Relation-like non empty finite set
bool [:{0},{m}:] is non empty finite V44() set
(((x2) ^ (x3)) ^ (x4)) ^ (m) is Relation-like T-Sequence-like Function-like finite set
(x2,x3,x4) is Relation-like 3 -defined T-Sequence-like Function-like total finite 3 -element set
((((x2) ^ (x3)) ^ (x4))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (((x2) ^ (x3)) ^ (x4)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(((x2) ^ (x3)) ^ (x4)) . 0 is set
(((x2) ^ (x3)) ^ (x4)) . 1 is set
(((x2) ^ (x3)) ^ (x4)) . 2 is set
((m)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (m) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() set
((((x2) ^ (x3)) ^ (x4))) + ((m)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
3 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 . ((((x2) ^ (x3)) ^ (x4))) is set
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 . 0 is set
x1 . 1 is set
x1 . 2 is set
x1 . 3 is set
x1 . 4 is set
x2 is set
(x2) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
x3 is set
(x3) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
(x2) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
x4 is set
(x4) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x4 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
((x2) ^ (x3)) ^ (x4) is Relation-like T-Sequence-like Function-like finite set
m is set
(m) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> m is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> m is Relation-like {0} -defined Function-like constant non empty total V25({0},{m}) finite Element of bool [:{0},{m}:]
{m} is non empty trivial finite 1 -element set
[:{0},{m}:] is Relation-like non empty finite set
bool [:{0},{m}:] is non empty finite V44() set
(((x2) ^ (x3)) ^ (x4)) ^ (m) is Relation-like T-Sequence-like Function-like finite set
l is set
(l) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> l is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> l is Relation-like {0} -defined Function-like constant non empty total V25({0},{l}) finite Element of bool [:{0},{l}:]
{l} is non empty trivial finite 1 -element set
[:{0},{l}:] is Relation-like non empty finite set
bool [:{0},{l}:] is non empty finite V44() set
((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l) is Relation-like T-Sequence-like Function-like finite set
(((((x2) ^ (x3)) ^ (x4)) ^ (m))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom ((((x2) ^ (x3)) ^ (x4)) ^ (m)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((((x2) ^ (x3)) ^ (x4)) ^ (m)) . 0 is set
((((x2) ^ (x3)) ^ (x4)) ^ (m)) . 1 is set
((((x2) ^ (x3)) ^ (x4)) ^ (m)) . 2 is set
((((x2) ^ (x3)) ^ (x4)) ^ (m)) . 3 is set
((l)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (l) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() set
(((((x2) ^ (x3)) ^ (x4)) ^ (m))) + ((l)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
4 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 . (((((x2) ^ (x3)) ^ (x4)) ^ (m))) is set
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 . 0 is set
x1 . 1 is set
x1 . 2 is set
x1 . 3 is set
x1 . 4 is set
x1 . 5 is set
x2 is set
(x2) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
x3 is set
(x3) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
(x2) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
x4 is set
(x4) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x4 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
((x2) ^ (x3)) ^ (x4) is Relation-like T-Sequence-like Function-like finite set
m is set
(m) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> m is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> m is Relation-like {0} -defined Function-like constant non empty total V25({0},{m}) finite Element of bool [:{0},{m}:]
{m} is non empty trivial finite 1 -element set
[:{0},{m}:] is Relation-like non empty finite set
bool [:{0},{m}:] is non empty finite V44() set
(((x2) ^ (x3)) ^ (x4)) ^ (m) is Relation-like T-Sequence-like Function-like finite set
l is set
(l) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> l is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> l is Relation-like {0} -defined Function-like constant non empty total V25({0},{l}) finite Element of bool [:{0},{l}:]
{l} is non empty trivial finite 1 -element set
[:{0},{l}:] is Relation-like non empty finite set
bool [:{0},{l}:] is non empty finite V44() set
((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l) is Relation-like T-Sequence-like Function-like finite set
R is set
(R) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> R is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> R is Relation-like {0} -defined Function-like constant non empty total V25({0},{R}) finite Element of bool [:{0},{R}:]
{R} is non empty trivial finite 1 -element set
[:{0},{R}:] is Relation-like non empty finite set
bool [:{0},{R}:] is non empty finite V44() set
(((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R) is Relation-like T-Sequence-like Function-like finite set
((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) . 0 is set
(((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) . 1 is set
(((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) . 2 is set
(((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) . 3 is set
(((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) . 4 is set
((R)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (R) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() set
((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l))) + ((R)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
5 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 . ((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l))) is set
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 . 0 is set
x1 . 1 is set
x1 . 2 is set
x1 . 3 is set
x1 . 4 is set
x1 . 5 is set
x1 . 6 is set
x2 is set
(x2) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
x3 is set
(x3) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
(x2) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
x4 is set
(x4) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x4 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
((x2) ^ (x3)) ^ (x4) is Relation-like T-Sequence-like Function-like finite set
m is set
(m) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> m is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> m is Relation-like {0} -defined Function-like constant non empty total V25({0},{m}) finite Element of bool [:{0},{m}:]
{m} is non empty trivial finite 1 -element set
[:{0},{m}:] is Relation-like non empty finite set
bool [:{0},{m}:] is non empty finite V44() set
(((x2) ^ (x3)) ^ (x4)) ^ (m) is Relation-like T-Sequence-like Function-like finite set
l is set
(l) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> l is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> l is Relation-like {0} -defined Function-like constant non empty total V25({0},{l}) finite Element of bool [:{0},{l}:]
{l} is non empty trivial finite 1 -element set
[:{0},{l}:] is Relation-like non empty finite set
bool [:{0},{l}:] is non empty finite V44() set
((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l) is Relation-like T-Sequence-like Function-like finite set
R is set
(R) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> R is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> R is Relation-like {0} -defined Function-like constant non empty total V25({0},{R}) finite Element of bool [:{0},{R}:]
{R} is non empty trivial finite 1 -element set
[:{0},{R}:] is Relation-like non empty finite set
bool [:{0},{R}:] is non empty finite V44() set
(((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R) is Relation-like T-Sequence-like Function-like finite set
j is set
(j) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> j is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> j is Relation-like {0} -defined Function-like constant non empty total V25({0},{j}) finite Element of bool [:{0},{j}:]
{j} is non empty trivial finite 1 -element set
[:{0},{j}:] is Relation-like non empty finite set
bool [:{0},{j}:] is non empty finite V44() set
((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j) is Relation-like T-Sequence-like Function-like finite set
(((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom ((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) . 0 is set
((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) . 1 is set
((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) . 2 is set
((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) . 3 is set
((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) . 4 is set
((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) . 5 is set
((j)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (j) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() set
(((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R))) + ((j)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
6 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 . (((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R))) is set
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 . 0 is set
x1 . 1 is set
x1 . 2 is set
x1 . 3 is set
x1 . 4 is set
x1 . 5 is set
x1 . 6 is set
x1 . 7 is set
x2 is set
(x2) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
x3 is set
(x3) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
(x2) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
x4 is set
(x4) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x4 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
((x2) ^ (x3)) ^ (x4) is Relation-like T-Sequence-like Function-like finite set
m is set
(m) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> m is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> m is Relation-like {0} -defined Function-like constant non empty total V25({0},{m}) finite Element of bool [:{0},{m}:]
{m} is non empty trivial finite 1 -element set
[:{0},{m}:] is Relation-like non empty finite set
bool [:{0},{m}:] is non empty finite V44() set
(((x2) ^ (x3)) ^ (x4)) ^ (m) is Relation-like T-Sequence-like Function-like finite set
l is set
(l) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> l is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> l is Relation-like {0} -defined Function-like constant non empty total V25({0},{l}) finite Element of bool [:{0},{l}:]
{l} is non empty trivial finite 1 -element set
[:{0},{l}:] is Relation-like non empty finite set
bool [:{0},{l}:] is non empty finite V44() set
((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l) is Relation-like T-Sequence-like Function-like finite set
R is set
(R) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> R is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> R is Relation-like {0} -defined Function-like constant non empty total V25({0},{R}) finite Element of bool [:{0},{R}:]
{R} is non empty trivial finite 1 -element set
[:{0},{R}:] is Relation-like non empty finite set
bool [:{0},{R}:] is non empty finite V44() set
(((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R) is Relation-like T-Sequence-like Function-like finite set
j is set
(j) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> j is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> j is Relation-like {0} -defined Function-like constant non empty total V25({0},{j}) finite Element of bool [:{0},{j}:]
{j} is non empty trivial finite 1 -element set
[:{0},{j}:] is Relation-like non empty finite set
bool [:{0},{j}:] is non empty finite V44() set
((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j) is Relation-like T-Sequence-like Function-like finite set
q is set
(q) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> q is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> q is Relation-like {0} -defined Function-like constant non empty total V25({0},{q}) finite Element of bool [:{0},{q}:]
{q} is non empty trivial finite 1 -element set
[:{0},{q}:] is Relation-like non empty finite set
bool [:{0},{q}:] is non empty finite V44() set
(((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q) is Relation-like T-Sequence-like Function-like finite set
((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) . 0 is set
(((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) . 1 is set
(((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) . 2 is set
(((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) . 3 is set
(((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) . 4 is set
(((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) . 5 is set
(((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) . 6 is set
((q)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (q) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() set
((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j))) + ((q)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
7 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 . ((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j))) is set
9 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 . 0 is set
x1 . 1 is set
x1 . 2 is set
x1 . 3 is set
x1 . 4 is set
x1 . 5 is set
x1 . 6 is set
x1 . 7 is set
x1 . 8 is set
x2 is set
(x2) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
x3 is set
(x3) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
(x2) ^ (x3) is Relation-like T-Sequence-like Function-like finite set
x4 is set
(x4) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x4 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
((x2) ^ (x3)) ^ (x4) is Relation-like T-Sequence-like Function-like finite set
m is set
(m) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> m is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> m is Relation-like {0} -defined Function-like constant non empty total V25({0},{m}) finite Element of bool [:{0},{m}:]
{m} is non empty trivial finite 1 -element set
[:{0},{m}:] is Relation-like non empty finite set
bool [:{0},{m}:] is non empty finite V44() set
(((x2) ^ (x3)) ^ (x4)) ^ (m) is Relation-like T-Sequence-like Function-like finite set
l is set
(l) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> l is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> l is Relation-like {0} -defined Function-like constant non empty total V25({0},{l}) finite Element of bool [:{0},{l}:]
{l} is non empty trivial finite 1 -element set
[:{0},{l}:] is Relation-like non empty finite set
bool [:{0},{l}:] is non empty finite V44() set
((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l) is Relation-like T-Sequence-like Function-like finite set
R is set
(R) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> R is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> R is Relation-like {0} -defined Function-like constant non empty total V25({0},{R}) finite Element of bool [:{0},{R}:]
{R} is non empty trivial finite 1 -element set
[:{0},{R}:] is Relation-like non empty finite set
bool [:{0},{R}:] is non empty finite V44() set
(((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R) is Relation-like T-Sequence-like Function-like finite set
j is set
(j) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> j is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> j is Relation-like {0} -defined Function-like constant non empty total V25({0},{j}) finite Element of bool [:{0},{j}:]
{j} is non empty trivial finite 1 -element set
[:{0},{j}:] is Relation-like non empty finite set
bool [:{0},{j}:] is non empty finite V44() set
((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j) is Relation-like T-Sequence-like Function-like finite set
q is set
(q) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> q is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> q is Relation-like {0} -defined Function-like constant non empty total V25({0},{q}) finite Element of bool [:{0},{q}:]
{q} is non empty trivial finite 1 -element set
[:{0},{q}:] is Relation-like non empty finite set
bool [:{0},{q}:] is non empty finite V44() set
(((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q) is Relation-like T-Sequence-like Function-like finite set
x is set
(x) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x is Relation-like {0} -defined Function-like constant non empty total V25({0},{x}) finite Element of bool [:{0},{x}:]
{x} is non empty trivial finite 1 -element set
[:{0},{x}:] is Relation-like non empty finite set
bool [:{0},{x}:] is non empty finite V44() set
((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q)) ^ (x) is Relation-like T-Sequence-like Function-like finite set
(((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom ((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q)) . 0 is set
((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q)) . 1 is set
((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q)) . 2 is set
((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q)) . 3 is set
((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q)) . 4 is set
((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q)) . 5 is set
((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q)) . 6 is set
((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q)) . 7 is set
((x)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (x) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() set
(((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q))) + ((x)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
8 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 . (((((((((x2) ^ (x3)) ^ (x4)) ^ (m)) ^ (l)) ^ (R)) ^ (j)) ^ (q))) is set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 . x1 is set
x3 is Relation-like T-Sequence-like Function-like finite set
x2 ^ x3 is Relation-like T-Sequence-like Function-like finite set
(x2 ^ x3) . x1 is set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 | x1 is Relation-like rng x2 -valued T-Sequence-like Function-like finite set
rng x2 is finite set
(x2) /\ x1 is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is Relation-like T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 | x1 is Relation-like rng x3 -valued T-Sequence-like Function-like finite set
rng x3 is finite set
(x3 | x1) . x2 is set
x3 . x2 is set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x3) /\ x1 is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x3 | x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 | x1 is Relation-like rng x2 -valued T-Sequence-like Function-like finite set
rng x2 is finite set
((x2 | x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x2 | x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
x2 | x1 is Relation-like rng x2 -valued T-Sequence-like Function-like finite set
rng x2 is finite set
((x2 | x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x2 | x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((x2 | x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 | x1 is Relation-like rng x2 -valued T-Sequence-like Function-like finite set
rng x2 is finite set
x2 . x1 is set
((x2 . x1)) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> (x2 . x1) is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> (x2 . x1) is Relation-like {0} -defined Function-like constant non empty total V25({0},{(x2 . x1)}) finite Element of bool [:{0},{(x2 . x1)}:]
{(x2 . x1)} is non empty trivial finite 1 -element set
[:{0},{(x2 . x1)}:] is Relation-like non empty finite set
bool [:{0},{(x2 . x1)}:] is non empty finite V44() set
(x2 | x1) ^ ((x2 . x1)) is Relation-like T-Sequence-like Function-like finite set
((x2 | x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x2 | x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x2 . m is set
((x2 | x1) ^ ((x2 . x1))) . m is set
((x2 | x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x2 | x1) ^ ((x2 . x1))) . m is set
(x2 | x1) . m is set
x2 . m is set
x2 . m is set
((x2 | x1) ^ ((x2 . x1))) . m is set
x2 . m is set
((x2 | x1) ^ ((x2 . x1))) . m is set
(((x2 | x1) ^ ((x2 . x1)))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom ((x2 | x1) ^ ((x2 . x1))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(((x2 . x1))) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom ((x2 . x1)) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() set
x1 + (((x2 . x1))) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 is Relation-like T-Sequence-like Function-like finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x2 is Relation-like T-Sequence-like Function-like finite set
x1 ^ x2 is Relation-like T-Sequence-like Function-like finite set
(x1 ^ x2) | (x1) is Relation-like rng (x1 ^ x2) -valued T-Sequence-like Function-like finite set
rng (x1 ^ x2) is finite set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1 ^ x2) . x4 is set
x1 . x4 is set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) + (x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x1 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x1 ^ x2)) /\ (x1) is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x1 ^ x2) | (x1)) . x4 is set
(((x1 ^ x2) | (x1))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom ((x1 ^ x2) | (x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x2 | x1 is Relation-like rng x2 -valued T-Sequence-like Function-like finite set
rng x2 is finite set
x3 is Relation-like T-Sequence-like Function-like finite set
x2 ^ x3 is Relation-like T-Sequence-like Function-like finite set
(x2 ^ x3) | x1 is Relation-like rng (x2 ^ x3) -valued T-Sequence-like Function-like finite set
rng (x2 ^ x3) is finite set
(x2 ^ x3) | (x2) is Relation-like rng (x2 ^ x3) -valued T-Sequence-like Function-like finite set
((x2 ^ x3) | (x2)) | x1 is Relation-like rng (x2 ^ x3) -valued rng ((x2 ^ x3) | (x2)) -valued T-Sequence-like Function-like finite set
rng ((x2 ^ x3) | (x2)) is finite set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is Relation-like T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x3) + x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 is Relation-like T-Sequence-like Function-like finite set
x3 ^ x4 is Relation-like T-Sequence-like Function-like finite set
(x3 ^ x4) | x1 is Relation-like rng (x3 ^ x4) -valued T-Sequence-like Function-like finite set
rng (x3 ^ x4) is finite set
x4 | x2 is Relation-like rng x4 -valued T-Sequence-like Function-like finite set
rng x4 is finite set
x3 ^ (x4 | x2) is Relation-like T-Sequence-like Function-like finite set
((x3 ^ x4)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x3 ^ x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) + (x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x3 ^ x4)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x3 ^ x4)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x3 ^ x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(((x3 ^ x4) | x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom ((x3 ^ x4) | x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) + (x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((x4 | x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x4 | x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((x3 ^ (x4 | x2))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x3 ^ (x4 | x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) + x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(((x3 ^ x4) | x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x3 ^ x4)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x3 ^ x4)) /\ x1 is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x3 ^ x4) | x1) . m is set
(x3 ^ x4) . m is set
(x3 ^ (x4 | x2)) . m is set
x3 . m is set
m - (x3) is ext-real V52() V55() set
x4 . (m - (x3)) is set
(m - (x3)) + (x3) is ext-real V52() V55() set
(x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x2 /\ (x4) is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x3 ^ (x4 | x2)) . m is set
(x4 | x2) . (m - (x3)) is set
(x3 ^ (x4 | x2)) . m is set
(x3 ^ (x4 | x2)) . m is set
((x3 ^ x4)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x3 ^ x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like T-Sequence-like Function-like finite set
x2 | x1 is Relation-like rng x2 -valued T-Sequence-like Function-like finite set
rng x2 is finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 ^ {} is Relation-like T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) - x1 is ext-real V52() V55() set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2) - x4 is ext-real V52() V55() set
x4 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(x2) - (x4 + 1) is ext-real V52() V55() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 | m is Relation-like rng x2 -valued T-Sequence-like Function-like finite set
m + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x2 | (m + 1) is Relation-like rng x2 -valued T-Sequence-like Function-like finite set
l is Relation-like T-Sequence-like Function-like finite set
(x2 | (m + 1)) ^ l is Relation-like T-Sequence-like Function-like finite set
(x2 | (m + 1)) | m is Relation-like rng x2 -valued rng (x2 | (m + 1)) -valued T-Sequence-like Function-like finite set
rng (x2 | (m + 1)) is finite set
(x2) - 0 is ext-real non negative V52() V55() set
((x2 | (m + 1))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x2 | (m + 1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x2 | (m + 1)) . m is set
(((x2 | (m + 1)) . m)) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> ((x2 | (m + 1)) . m) is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> ((x2 | (m + 1)) . m) is Relation-like {0} -defined Function-like constant non empty total V25({0},{((x2 | (m + 1)) . m)}) finite Element of bool [:{0},{((x2 | (m + 1)) . m)}:]
{((x2 | (m + 1)) . m)} is non empty trivial finite 1 -element set
[:{0},{((x2 | (m + 1)) . m)}:] is Relation-like non empty finite set
bool [:{0},{((x2 | (m + 1)) . m)}:] is non empty finite V44() set
((x2 | (m + 1)) | m) ^ (((x2 | (m + 1)) . m)) is Relation-like T-Sequence-like Function-like finite set
(((x2 | (m + 1)) . m)) ^ l is Relation-like T-Sequence-like Function-like finite set
(x2 | m) ^ ((((x2 | (m + 1)) . m)) ^ l) is Relation-like T-Sequence-like Function-like finite set
(x2) - 0 is ext-real non negative V52() V55() set
x2 | ((x2) - 0) is Relation-like Function-like finite set
x2 ^ {} is Relation-like T-Sequence-like Function-like finite set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 | x4 is Relation-like rng x2 -valued T-Sequence-like Function-like finite set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x2) - x3 is ext-real V52() V55() set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is Relation-like T-Sequence-like Function-like finite set
(x2 | x1) ^ x3 is Relation-like T-Sequence-like Function-like finite set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 + x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is Relation-like T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
m is Relation-like T-Sequence-like Function-like finite set
(m) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
R is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
l + R is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
j is Relation-like T-Sequence-like Function-like finite set
(j) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
q is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() set
(q) is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() Element of NAT
dom q is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() set
j ^ q is Relation-like T-Sequence-like Function-like finite set
m ^ {} is Relation-like T-Sequence-like Function-like finite set
j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
j + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
q is Relation-like T-Sequence-like Function-like finite set
x is set
(x) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x is Relation-like {0} -defined Function-like constant non empty total V25({0},{x}) finite Element of bool [:{0},{x}:]
{x} is non empty trivial finite 1 -element set
[:{0},{x}:] is Relation-like non empty finite set
bool [:{0},{x}:] is non empty finite V44() set
q ^ (x) is Relation-like T-Sequence-like Function-like finite set
(q) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((x)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (x) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() set
(q) + ((x)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(q) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
l + j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
q1 is Relation-like T-Sequence-like Function-like finite set
(q1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom q1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
q2 is Relation-like T-Sequence-like Function-like finite set
(q2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom q2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
q1 ^ q2 is Relation-like T-Sequence-like Function-like finite set
q2 ^ (x) is Relation-like T-Sequence-like Function-like finite set
((q2 ^ (x))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (q2 ^ (x)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(q2) + ((x)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
q1 ^ (q2 ^ (x)) is Relation-like T-Sequence-like Function-like finite set
x4 is Relation-like T-Sequence-like Function-like finite set
(x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
m + l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
{} ^ {} is Relation-like T-Sequence-like Function-like finite set
({}) is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() Element of NAT
dom {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() set
x1 is set
(x1) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
x2 is set
(x2) is Relation-like 1 -defined T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
x3 is Relation-like T-Sequence-like Function-like finite set
(x1) ^ x3 is Relation-like T-Sequence-like Function-like finite set
x4 is Relation-like T-Sequence-like Function-like finite set
(x2) ^ x4 is Relation-like T-Sequence-like Function-like finite set
((x1) ^ x3) . 0 is set
x1 is set
x2 is Relation-like NAT -defined x1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x1
len x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x3 is Relation-like T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is Relation-like T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
rng x3 is finite set
x4 is set
rng x2 is finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
m is set
x3 . m is set
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
l + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
Seg (len x2) is finite len x2 -element V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
dom x2 is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x2 . (l + 1) is set
x3 . l is set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x2 . (x4 + 1) is set
x3 . x4 is set
x3 is Relation-like x1 -valued T-Sequence-like Function-like finite set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 is Relation-like x1 -valued T-Sequence-like Function-like finite set
(x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 . m is set
x4 . m is set
m + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x2 . (m + 1) is set
x1 is set
x2 is Relation-like x1 -valued T-Sequence-like Function-like finite set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
rng x3 is finite set
x4 is set
rng x2 is finite set
m is set
x3 . m is set
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
Seg (x2) is finite (x2) -element V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
l - 1 is ext-real V52() V55() set
l -' 1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(l -' 1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x2 . (l -' 1) is set
x3 . l is set
Seg (x2) is finite (x2) -element V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 -' 1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x2 . (x4 -' 1) is set
x3 . x4 is set
x3 is Relation-like NAT -defined x1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x1
len x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 is Relation-like NAT -defined x1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x1
len x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 . m is set
x4 . m is set
m -' 1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x2 . (m -' 1) is set
x3 is set
x1 is set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 --> x3 is Relation-like x2 -defined T-Sequence-like Function-like constant total V25(x2,{x3}) finite Element of bool [:x2,{x3}:]
{x3} is non empty trivial finite 1 -element set
[:x2,{x3}:] is Relation-like finite set
bool [:x2,{x3}:] is non empty finite V44() set
x1 is non empty set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is Relation-like NAT -defined x1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x1
len x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x3 -' (len x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x3 -' (len x2)) -' 1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
m is Element of x1
((x3 -' (len x2)) -' 1) --> m is Relation-like (x3 -' (len x2)) -' 1 -defined x1 -valued T-Sequence-like Function-like constant total V25((x3 -' (len x2)) -' 1,x1) finite Element of bool [:((x3 -' (len x2)) -' 1),x1:]
[:((x3 -' (len x2)) -' 1),x1:] is Relation-like set
bool [:((x3 -' (len x2)) -' 1),x1:] is non empty set
{m} is non empty trivial finite 1 -element set
[:((x3 -' (len x2)) -' 1),{m}:] is Relation-like finite set
x4 is Element of x1
(x4) is Relation-like 1 -defined x1 -valued T-Sequence-like Function-like constant non empty trivial total finite 1 -element set
0 .--> x4 is Relation-like NAT -defined {0} -defined x1 -valued Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined x1 -valued Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
(x1,x2) is Relation-like x1 -valued T-Sequence-like Function-like finite set
(x4) ^ (x1,x2) is Relation-like x1 -valued T-Sequence-like Function-like finite set
l is Relation-like x1 -valued T-Sequence-like Function-like finite set
((x4) ^ (x1,x2)) ^ l is Relation-like x1 -valued T-Sequence-like Function-like finite set
((x4)) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
((x4)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (x4) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() set
((x1,x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1,x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
((x4)) + ((x1,x2)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(((x4) ^ (x1,x2))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom ((x4) ^ (x1,x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
R is Relation-like x1 -valued T-Sequence-like Function-like non empty finite set
R . 0 is set
((x4) ^ (x1,x2)) . 0 is set
(x4) . 0 is set
j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
R . j is set
x2 . j is set
j - 1 is ext-real V52() V55() set
j -' 1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
j + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(j + 1) - 1 is ext-real V52() V55() set
1 + (len x2) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
1 + (j -' 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
((x4) ^ (x1,x2)) . (1 + (j -' 1)) is set
(x1,x2) . (j -' 1) is set
(j -' 1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x2 . ((j -' 1) + 1) is set
x3 - (len x2) is ext-real V52() V55() set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(x3 -' (len x2)) - 1 is ext-real V52() V55() set
(l) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
j is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
R . j is set
1 + (len x2) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(len x2) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x3 - ((len x2) + 1) is ext-real V52() V55() set
j - (1 + (len x2)) is ext-real V52() V55() set
j -' (1 + (len x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
j - ((len x2) + 1) is ext-real V52() V55() set
j -' (((x4) ^ (x1,x2))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(((x4) ^ (x1,x2))) + (j -' (((x4) ^ (x1,x2)))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
l . (j -' (((x4) ^ (x1,x2)))) is set
(R) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom R is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() set
(((x4) ^ (x1,x2))) + (l) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(((x4)) + ((x1,x2))) + (l) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
1 + ((x1,x2)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(1 + ((x1,x2))) + (l) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
1 + (len x2) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(1 + (len x2)) + (l) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(1 + (len x2)) + ((x3 -' (len x2)) -' 1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
(len x2) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x3 - ((len x2) + 1) is ext-real V52() V55() set
(x3 - ((len x2) + 1)) + ((len x2) + 1) is ext-real V52() V55() set
x4 is Relation-like x1 -valued T-Sequence-like Function-like non empty finite set
x4 . 0 is set
(x4) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom x4 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() set
m is Relation-like x1 -valued T-Sequence-like Function-like non empty finite set
m . 0 is set
(m) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom m is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() set
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 . l is set
m . l is set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x2 . l is set
x1 is non empty set
x2 is Relation-like x1 -valued T-Sequence-like Function-like finite set
x2 . 0 is set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x4 is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x4 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x4 is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
rng x4 is finite set
m is set
l is set
x4 . l is set
R is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
Seg x3 is finite x3 -element V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x2 . R is set
rng x2 is finite set
Seg x3 is finite x3 -element V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
m is Relation-like NAT -defined x1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x1
len m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
R is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
m . R is set
x2 . R is set
R is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
m . R is set
x2 . R is set
x4 is Relation-like NAT -defined x1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x1
len x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
m is Relation-like NAT -defined x1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x1
len m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 . l is set
m . l is set
x2 . l is set
x1 is non empty set
x2 is Relation-like x1 -valued T-Sequence-like Function-like finite set
x2 . 0 is set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1,x2) is Relation-like NAT -defined x1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of x1
len (x1,x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like Function-like set
dom x1 is set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is Relation-like T-Sequence-like Function-like finite set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is Relation-like T-Sequence-like Function-like finite () set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is Relation-like NAT -defined Function-like non empty () set
dom x1 is non empty V66() V67() V68() V69() V70() V71() V78() V80() set
x2 is set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like Function-like set
dom x1 is set
x2 is set
x4 is set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x2 is set
x3 is set
x4 is epsilon-transitive epsilon-connected ordinal set
m is epsilon-transitive epsilon-connected ordinal set
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
card x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
x3 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
card x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is Relation-like NAT -defined Function-like () set
dom x1 is V66() V67() V68() V69() V70() V71() V80() set
x2 is Relation-like NAT -defined Function-like set
dom x2 is V66() V67() V68() V69() V70() V71() V80() set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
card x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT : not card x1 <= b₁ } is set
x2 is set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x2 is set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like NAT -defined T-Sequence-like Function-like non empty finite () set
LastLoc x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
K364(NAT,x1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
K349(K364(NAT,x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() set
x2 is Relation-like NAT -defined Function-like non empty finite set
LastLoc x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
K364(NAT,x2) is non empty finite V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
K349(K364(NAT,x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() set
(x1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
dom x2 is non empty finite V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
x3 is set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like NAT -defined T-Sequence-like Function-like non empty finite () set
LastLoc x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
K364(NAT,x1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
K349(K364(NAT,x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() set
card x1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
(card x1) -' 1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
((card x1) -' 1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x3 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x3 + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like NAT -defined T-Sequence-like Function-like non empty finite () set
FirstLoc x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
K364(NAT,x1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
K350(K364(NAT,x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() set
x1 is Relation-like NAT -defined T-Sequence-like Function-like non empty finite () set
CutLastLoc x1 is Relation-like NAT -defined Function-like finite set
LastLoc x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
K364(NAT,x1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
K349(K364(NAT,x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() set
x1 . (LastLoc x1) is set
(LastLoc x1) .--> (x1 . (LastLoc x1)) is Relation-like NAT -defined {(LastLoc x1)} -defined Function-like one-to-one finite set
{(LastLoc x1)} is non empty trivial finite V44() 1 -element V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
{(LastLoc x1)} --> (x1 . (LastLoc x1)) is Relation-like {(LastLoc x1)} -defined Function-like constant non empty total V25({(LastLoc x1)},{(x1 . (LastLoc x1))}) finite Element of bool [:{(LastLoc x1)},{(x1 . (LastLoc x1))}:]
{(x1 . (LastLoc x1))} is non empty trivial finite 1 -element set
[:{(LastLoc x1)},{(x1 . (LastLoc x1))}:] is Relation-like non empty finite set
bool [:{(LastLoc x1)},{(x1 . (LastLoc x1))}:] is non empty finite V44() set
x1 \ ((LastLoc x1) .--> (x1 . (LastLoc x1))) is Relation-like NAT -defined Function-like finite Element of bool x1
bool x1 is non empty finite V44() set
x3 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative Function-yielding V39() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V52() V55() V66() V67() V68() V69() V70() V71() V72() V80() V81() V82() V83() () set
x3 is Relation-like Function-like non empty finite set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
dom x3 is non empty finite set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
[(LastLoc x1),(x1 . (LastLoc x1))] is set
{(LastLoc x1),(x1 . (LastLoc x1))} is non empty finite set
{{(LastLoc x1),(x1 . (LastLoc x1))},{(LastLoc x1)}} is non empty finite V44() set
{[(LastLoc x1),(x1 . (LastLoc x1))]} is Relation-like Function-like constant non empty trivial finite 1 -element set
R is Relation-like set
dom R is set
(x1) \ (dom R) is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x1 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
card x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
x2 is Relation-like Function-like set
Shift (x2,(card x1)) is Relation-like NAT -defined Function-like set
dom (Shift (x2,(card x1))) is V66() V67() V68() V69() V70() V71() V80() set
dom x2 is set
{ (b₁ + (card x1)) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT : b₁ in dom x2 } is set
x3 is set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 + (card x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
succ x2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() set
{x2} is non empty trivial finite V44() 1 -element V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
x2 \/ {x2} is non empty finite set
x2 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
card x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
x1 is set
(x1) is non empty set
x2 is set
x1 is set
(x1) is functional non empty set
x2 is Relation-like Function-like Element of (x1)
x3 is Relation-like Function-like Element of (x1)
x1 is set
x2 is Relation-like NAT -defined x1 -valued T-Sequence-like Function-like finite () set
(x1) is functional non empty set
x1 is set
(x1) is functional non empty set
x2 is Relation-like NAT -defined x1 -valued T-Sequence-like Function-like finite () set
x3 is Relation-like NAT -defined T-Sequence-like Function-like finite () Element of (x1)
x2 ^ x3 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x4 is Relation-like NAT -defined x1 -valued T-Sequence-like Function-like finite () set
x2 ^ x4 is Relation-like NAT -defined x1 -valued T-Sequence-like Function-like finite () set
x1 is set
(x1) is functional non empty set
x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () Element of (x1)
x3 is Relation-like NAT -defined T-Sequence-like Function-like finite () Element of (x1)
x2 ^ x3 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x4 is Relation-like NAT -defined x1 -valued T-Sequence-like Function-like finite () set
m is Relation-like NAT -defined x1 -valued T-Sequence-like Function-like finite () set
x4 ^ m is Relation-like NAT -defined x1 -valued T-Sequence-like Function-like finite () set
x1 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x1 ^ x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x1 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x3 is set
(x1 ^ x2) . x3 is set
x1 . x3 is set
x1 is set
(x1) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x2 ^ (x1) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
((x2 ^ (x1))) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x2 ^ (x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
(x2) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
((x1)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
dom (x1) is epsilon-transitive epsilon-connected ordinal natural non empty trivial ext-real positive non negative finite cardinal 1 -element V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
(x2) + ((x1)) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 is set
x2 is set
(x1,x2) is Relation-like NAT -defined T-Sequence-like Function-like finite 2 -element () set
(x1) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
(x2) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(0,1) --> (x1,x2) is finite set
((x1,x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal 2 -element V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
((x1,x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1,x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal 2 -element V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
{0,1} is non empty finite V44() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
(x1,x2) . 0 is set
(x1,x2) . 1 is set
x1 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
card x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x1 ^ x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
Shift (x2,(card x1)) is Relation-like NAT -defined Function-like finite set
x1 +* (Shift (x2,(card x1))) is Relation-like Function-like finite set
dom (Shift (x2,(card x1))) is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
{ (b₁ + (card x1)) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT : b₁ in (x2) } is set
((x1 ^ x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
x3 is set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) + m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 + (card x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x1) \/ (dom (Shift (x2,(card x1)))) is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() set
x3 is set
(x1 ^ x2) . x3 is set
(Shift (x2,(card x1))) . x3 is set
x1 . x3 is set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
m + (card x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
(x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x4 -' (x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
(x1) + (x4 -' (x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x2 . (x4 -' (x1)) is set
x1 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x1 ^ x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x1 +* (x1 ^ x2) is Relation-like Function-like finite set
(x1 ^ x2) +* x1 is Relation-like Function-like finite set
x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
Shift (x2,x1) is Relation-like NAT -defined Function-like finite set
dom (Shift (x2,x1)) is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() set
card x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
x1 + (card x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x3 is Relation-like Function-like set
Shift (x3,(x1 + (card x2))) is Relation-like NAT -defined Function-like set
dom (Shift (x3,(x1 + (card x2)))) is V66() V67() V68() V69() V70() V71() V80() set
dom x3 is set
{ (b₁ + (x1 + (card x2))) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT : b₁ in dom x3 } is set
x4 is set
(x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
{ (b₁ + x1) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT : b₁ in (x2) } is set
m is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
m + x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
l is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
l + (x1 + (card x2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x1 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x1 ^ x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
Shift (x1,x3) is Relation-like NAT -defined Function-like finite set
Shift ((x1 ^ x2),x3) is Relation-like NAT -defined Function-like finite set
card x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
Shift (x2,(card x1)) is Relation-like NAT -defined Function-like finite set
x1 +* (Shift (x2,(card x1))) is Relation-like Function-like finite set
Shift ((Shift (x2,(card x1))),x3) is Relation-like NAT -defined Function-like finite set
(Shift (x1,x3)) +* (Shift ((Shift (x2,(card x1))),x3)) is Relation-like Function-like finite set
x3 + (card x1) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
Shift (x2,(x3 + (card x1))) is Relation-like NAT -defined Function-like finite set
dom (Shift (x1,x3)) is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() set
dom (Shift ((Shift (x2,(card x1))),x3)) is finite V66() V67() V68() V69() V70() V71() V80() V81() V82() set
x1 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
card x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
x2 ^ x1 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x3 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
x3 + (card x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
Shift (x1,(x3 + (card x2))) is Relation-like NAT -defined Function-like finite set
Shift ((x2 ^ x1),x3) is Relation-like NAT -defined Function-like finite set
Shift (x1,(card x2)) is Relation-like NAT -defined Function-like finite set
Shift ((Shift (x1,(card x2))),x3) is Relation-like NAT -defined Function-like finite set
x2 +* (Shift (x1,(card x2))) is Relation-like Function-like finite set
Shift (x2,x3) is Relation-like NAT -defined Function-like finite set
(Shift (x2,x3)) +* (Shift ((Shift (x1,(card x2))),x3)) is Relation-like Function-like finite set
x1 is set
x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x3 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x2 ^ x3 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
Shift ((x2 ^ x3),x4) is Relation-like NAT -defined Function-like finite set
Shift (x2,x4) is Relation-like NAT -defined Function-like finite set
x1 is set
x2 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
card x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom x2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
x3 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x2 ^ x3 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x4 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
Shift ((x2 ^ x3),x4) is Relation-like NAT -defined Function-like finite set
x4 + (card x2) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
Shift (x3,(x4 + (card x2))) is Relation-like NAT -defined Function-like finite set
x1 is Relation-like NAT -defined T-Sequence-like Function-like non empty finite () set
CutLastLoc x1 is Relation-like NAT -defined T-Sequence-like Function-like finite () set
LastLoc x1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
K364(NAT,x1) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of bool NAT
K349(K364(NAT,x1)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() set
x1 . (LastLoc x1) is set
(LastLoc x1) .--> (x1 . (LastLoc x1)) is Relation-like NAT -defined {(LastLoc x1)} -defined Function-like one-to-one finite set
{(LastLoc x1)} is non empty trivial finite V44() 1 -element V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() set
{(LastLoc x1)} --> (x1 . (LastLoc x1)) is Relation-like {(LastLoc x1)} -defined Function-like constant non empty total V25({(LastLoc x1)},{(x1 . (LastLoc x1))}) finite Element of bool [:{(LastLoc x1)},{(x1 . (LastLoc x1))}:]
{(x1 . (LastLoc x1))} is non empty trivial finite 1 -element set
[:{(LastLoc x1)},{(x1 . (LastLoc x1))}:] is Relation-like non empty finite set
bool [:{(LastLoc x1)},{(x1 . (LastLoc x1))}:] is non empty finite V44() set
x1 \ ((LastLoc x1) .--> (x1 . (LastLoc x1))) is Relation-like NAT -defined Function-like finite Element of bool x1
bool x1 is non empty finite V44() set
x1 is set
(x1) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
x2 is set
(x2) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x3 is set
(x3) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
((x1) ^ (x2)) ^ (x3) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x4 is set
(x4) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x4 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
(((x1) ^ (x2)) ^ (x3)) ^ (x4) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x1 is set
x2 is set
x3 is set
x4 is set
(x1,x2,x3,x4) is set
(x1) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
(x2) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x3) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
((x1) ^ (x2)) ^ (x3) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x4) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x4 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
(((x1) ^ (x2)) ^ (x3)) ^ (x4) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x1 is set
x2 is set
x3 is set
x4 is set
(x1,x2,x3,x4) is Relation-like Function-like set
(x1) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
(x2) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x3) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
((x1) ^ (x2)) ^ (x3) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x4) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x4 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
(((x1) ^ (x2)) ^ (x3)) ^ (x4) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
x1 is set
x2 is set
x3 is set
x4 is set
(x1,x2,x3,x4) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x1) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
(x2) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x3) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
((x1) ^ (x2)) ^ (x3) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x4) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x4 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
(((x1) ^ (x2)) ^ (x3)) ^ (x4) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
((x1,x2,x3,x4)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1,x2,x3,x4) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
(x1,x2,x3) is Relation-like NAT -defined T-Sequence-like Function-like finite 3 -element () set
((x1,x2,x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1,x2,x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal 3 -element V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
((x1,x2,x3)) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
3 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V78() V79() V80() V81() V82() Element of NAT
x1 is set
x2 is set
x3 is set
x4 is set
(x1,x2,x3,x4) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x1) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x1 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x1 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x1}) finite Element of bool [:{0},{x1}:]
{x1} is non empty trivial finite 1 -element set
[:{0},{x1}:] is Relation-like non empty finite set
bool [:{0},{x1}:] is non empty finite V44() set
(x2) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x2 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x2 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x2}) finite Element of bool [:{0},{x2}:]
{x2} is non empty trivial finite 1 -element set
[:{0},{x2}:] is Relation-like non empty finite set
bool [:{0},{x2}:] is non empty finite V44() set
(x1) ^ (x2) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x3) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x3 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x3 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x3}) finite Element of bool [:{0},{x3}:]
{x3} is non empty trivial finite 1 -element set
[:{0},{x3}:] is Relation-like non empty finite set
bool [:{0},{x3}:] is non empty finite V44() set
((x1) ^ (x2)) ^ (x3) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x4) is Relation-like NAT -defined T-Sequence-like Function-like constant non empty trivial finite 1 -element () set
0 .--> x4 is Relation-like NAT -defined {0} -defined Function-like one-to-one finite set
{0} --> x4 is Relation-like {0} -defined Function-like constant non empty total V25({0},{x4}) finite Element of bool [:{0},{x4}:]
{x4} is non empty trivial finite 1 -element set
[:{0},{x4}:] is Relation-like non empty finite set
bool [:{0},{x4}:] is non empty finite V44() set
(((x1) ^ (x2)) ^ (x3)) ^ (x4) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x1,x2,x3,x4) . 0 is set
(x1,x2,x3,x4) . 1 is set
(x1,x2,x3,x4) . 2 is set
(x1,x2,x3,x4) . 3 is set
(x2,x3) is Relation-like NAT -defined T-Sequence-like Function-like finite 2 -element () set
(x2) ^ (x3) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x1) ^ (x2,x3) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
((x1) ^ (x2,x3)) ^ (x4) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(((x1) ^ (x2,x3)) ^ (x4)) . 0 is set
(x2,x3,x4) is Relation-like NAT -defined T-Sequence-like Function-like finite 3 -element () set
((x2) ^ (x3)) ^ (x4) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
(x1) ^ (x2,x3,x4) is Relation-like NAT -defined T-Sequence-like Function-like finite () set
((x1) ^ (x2,x3,x4)) . 0 is set
(x1,x2,x3) is Relation-like NAT -defined T-Sequence-like Function-like finite 3 -element () set
((x1,x2,x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V53() V54() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of NAT
dom (x1,x2,x3) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal 3 -element V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() set
((x1,x2,x3)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal 3 -element V52() V55() V66() V67() V68() V69() V70() V71() V80() V81() V82() Element of bool NAT
(x1,x2,x3) . 1 is set
(x1,x2,x3) . 2 is set