:: 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

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

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

x1 is set

{ b

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

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

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}}