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
{ b1 where b1 is epsilon-transitive epsilon-connected 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 <= b1 } 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
{ b1 where b1 is epsilon-transitive epsilon-connected 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) <= b1 } 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
F1() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal V52() V55() set
x1 is set
{ b1 where b1 is epsilon-transitive epsilon-connected 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 F1() <= b1 } 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
F1() 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
F2(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}}