:: AFINSQ_2 semantic presentation

REAL is non empty V12() non finite complex-membered ext-real-membered real-membered V56() set

NAT is non empty V12() epsilon-transitive epsilon-connected ordinal non finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() cardinal limit_cardinal Element of K19(REAL)

K19(REAL) is V12() non finite set

COMPLEX is non empty V12() non finite complex-membered V56() set

RAT is non empty V12() non finite complex-membered ext-real-membered real-membered rational-membered V56() set

INT is non empty V12() non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V56() set

K20(NAT,REAL) is Relation-like V12() complex-valued ext-real-valued real-valued non finite set

K19(K20(NAT,REAL)) is V12() non finite set

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V86() set

the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V86() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V86() set

1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

{{},1} is non empty finite V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

NAT is non empty V12() epsilon-transitive epsilon-connected ordinal non finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() cardinal limit_cardinal set

K19(NAT) is V12() non finite set

K19(NAT) is V12() non finite set

K249(NAT) is V70() set

K20(COMPLEX,COMPLEX) is Relation-like V12() complex-valued non finite set

K19(K20(COMPLEX,COMPLEX)) is V12() non finite set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like V12() complex-valued non finite set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() non finite set

K20(REAL,REAL) is Relation-like V12() complex-valued ext-real-valued real-valued non finite set

K19(K20(REAL,REAL)) is V12() non finite set

K20(K20(REAL,REAL),REAL) is Relation-like V12() complex-valued ext-real-valued real-valued non finite set

K19(K20(K20(REAL,REAL),REAL)) is V12() non finite set

K20(RAT,RAT) is Relation-like RAT -valued V12() complex-valued ext-real-valued real-valued non finite set

K19(K20(RAT,RAT)) is V12() non finite set

K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued V12() complex-valued ext-real-valued real-valued non finite set

K19(K20(K20(RAT,RAT),RAT)) is V12() non finite set

K20(INT,INT) is Relation-like RAT -valued INT -valued V12() complex-valued ext-real-valued real-valued non finite set

K19(K20(INT,INT)) is V12() non finite set

K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued V12() complex-valued ext-real-valued real-valued non finite set

K19(K20(K20(INT,INT),INT)) is V12() non finite set

K20(NAT,NAT) is Relation-like RAT -valued INT -valued V12() complex-valued ext-real-valued real-valued natural-valued non finite set

K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V12() complex-valued ext-real-valued real-valued natural-valued non finite set

K19(K20(K20(NAT,NAT),NAT)) is V12() non finite set

2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real complex-valued ext-real-valued real-valued natural-valued integer finite finite-yielding V48() rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V86() Element of NAT

dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V86() set

rng {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real complex-valued ext-real-valued real-valued natural-valued V37() decreasing non-decreasing non-increasing finite finite-yielding V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V82() V86() set

card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V86() set

{{}} is functional non empty V12() finite V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered 1 -element set

addcomplex is Relation-like K20(COMPLEX,COMPLEX) -defined COMPLEX -valued Function-like V14(K20(COMPLEX,COMPLEX)) quasi_total complex-valued having_a_unity commutative associative Element of K19(K20(K20(COMPLEX,COMPLEX),COMPLEX))

addreal is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like V14(K20(REAL,REAL)) quasi_total complex-valued ext-real-valued real-valued having_a_unity commutative associative Element of K19(K20(K20(REAL,REAL),REAL))

addrat is Relation-like K20(RAT,RAT) -defined RAT -valued Function-like V14(K20(RAT,RAT)) quasi_total complex-valued ext-real-valued real-valued having_a_unity commutative associative Element of K19(K20(K20(RAT,RAT),RAT))

addint is Relation-like K20(INT,INT) -defined INT -valued Function-like V14(K20(INT,INT)) quasi_total complex-valued ext-real-valued real-valued having_a_unity commutative associative Element of K19(K20(K20(INT,INT),INT))

addnat is Relation-like K20(NAT,NAT) -defined NAT -valued INT -valued Function-like V14(K20(NAT,NAT)) quasi_total complex-valued ext-real-valued real-valued natural-valued having_a_unity commutative associative Element of K19(K20(K20(NAT,NAT),NAT))

the_unity_wrt addcomplex is complex Element of COMPLEX

the_unity_wrt addreal is ext-real complex real Element of REAL

the_unity_wrt addrat is ext-real complex real rational Element of RAT

the_unity_wrt addint is ext-real complex real integer rational Element of INT

the_unity_wrt addnat is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

x is finite set

p is finite set

card x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

card p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

p \ x is finite Element of K19(p)

K19(p) is finite V48() set

card (p \ x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(card p) - (card x) is ext-real complex real integer rational Element of INT

x is finite set

p is finite set

K20(x,p) is Relation-like finite set

K19(K20(x,p)) is finite V48() set

card x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

card p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

q is Relation-like x -defined p -valued Function-like quasi_total finite Element of K19(K20(x,p))

dom q is finite Element of K19(x)

K19(x) is finite V48() set

y is set

r is set

q . y is set

q . r is set

{y} is non empty V12() finite 1 -element set

x \ {y} is finite Element of K19(x)

c

q .: c

K19(p) is finite V48() set

c is set

rng q is finite Element of K19(p)

b is set

q . b is set

card c

dom q is finite Element of K19(x)

K19(x) is finite V48() set

q .: (dom q) is finite Element of K19(p)

K19(p) is finite V48() set

card (dom q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

card (q .: (dom q)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

rng q is finite Element of K19(p)

y is set

card (rng q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

{y} is non empty V12() finite 1 -element set

p \ {y} is finite Element of K19(p)

card (p \ {y}) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite cardinal set

p is set

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite cardinal set

p is set

x is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set

p is Relation-like Function-like set

rng p is set

dom p is set

q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

y is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

r is Relation-like NAT -defined NAT -valued Function-like T-Sequence-like complex-valued ext-real-valued real-valued natural-valued finite V86() set

dom r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

c

c

c

(c

c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

len r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(c

r . c

(r . c

max (c,((r . c

k1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

r . k1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

len r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(c

b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

r . b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

len r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(c

0 -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

c

r . c

len r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(len r) -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

c

rng r is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of K19(NAT)

c is set

b is set

r . b is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(len r) - 1 is ext-real complex real integer rational Element of INT

0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

x is set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

rng p is finite set

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

q is set

p . q is set

x is set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

rng p is finite set

q is set

y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

p . y is set

F

F

x is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

x . p is set

q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

x . q is set

F

p is Relation-like NAT -defined F

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p . q is set

F

the Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V86() set is Relation-like non-empty empty-yielding NAT -defined NAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V86() set

x is Relation-like Function-like T-Sequence-like complex-valued set

- x is Relation-like Function-like complex-valued set

- 1 is ext-real non positive complex real set

(- 1) (#) x is Relation-like Function-like complex-valued set

dom x is epsilon-transitive epsilon-connected ordinal set

dom (- x) is set

x " is Relation-like Function-like complex-valued set

dom x is epsilon-transitive epsilon-connected ordinal set

dom (x ") is set

x ^2 is Relation-like Function-like complex-valued set

x (#) x is Relation-like Function-like complex-valued set

dom x is epsilon-transitive epsilon-connected ordinal set

dom (x ^2) is set

|.x.| is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom x is epsilon-transitive epsilon-connected ordinal set

dom |.x.| is set

p is Relation-like Function-like T-Sequence-like complex-valued set

x + p is Relation-like Function-like complex-valued set

dom (x + p) is set

dom x is epsilon-transitive epsilon-connected ordinal set

dom p is epsilon-transitive epsilon-connected ordinal set

(dom x) /\ (dom p) is epsilon-transitive epsilon-connected ordinal set

x - p is Relation-like Function-like complex-valued set

- p is Relation-like Function-like T-Sequence-like complex-valued set

(- 1) (#) p is Relation-like Function-like complex-valued set

x + (- p) is Relation-like Function-like T-Sequence-like complex-valued set

x (#) p is Relation-like Function-like complex-valued set

dom (x (#) p) is set

dom x is epsilon-transitive epsilon-connected ordinal set

dom p is epsilon-transitive epsilon-connected ordinal set

(dom x) /\ (dom p) is epsilon-transitive epsilon-connected ordinal set

x /" p is Relation-like Function-like complex-valued set

p " is Relation-like Function-like T-Sequence-like complex-valued set

x (#) (p ") is Relation-like Function-like T-Sequence-like complex-valued set

x is Relation-like Function-like complex-valued finite set

- x is Relation-like Function-like complex-valued set

(- 1) (#) x is Relation-like Function-like complex-valued set

dom x is finite set

dom (- x) is set

x " is Relation-like Function-like complex-valued set

dom x is finite set

dom (x ") is set

x ^2 is Relation-like Function-like complex-valued set

x (#) x is Relation-like Function-like complex-valued set

dom x is finite set

dom (x ^2) is set

|.x.| is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom x is finite set

dom |.x.| is set

p is Relation-like Function-like complex-valued set

x + p is Relation-like Function-like complex-valued set

dom (x + p) is set

dom x is finite set

dom p is set

(dom x) /\ (dom p) is finite set

x - p is Relation-like Function-like complex-valued set

- p is Relation-like Function-like complex-valued set

(- 1) (#) p is Relation-like Function-like complex-valued set

x + (- p) is Relation-like Function-like complex-valued finite set

x (#) p is Relation-like Function-like complex-valued set

dom (x (#) p) is set

dom x is finite set

dom p is set

(dom x) /\ (dom p) is finite set

x /" p is Relation-like Function-like complex-valued set

p " is Relation-like Function-like complex-valued set

x (#) (p ") is Relation-like Function-like complex-valued finite set

p /" x is Relation-like Function-like complex-valued set

p (#) (x ") is Relation-like Function-like complex-valued finite set

x is Relation-like Function-like T-Sequence-like complex-valued set

p is complex set

p + x is Relation-like Function-like complex-valued set

dom x is epsilon-transitive epsilon-connected ordinal set

dom (p + x) is set

x - p is Relation-like Function-like complex-valued set

- p is complex set

(- p) + x is Relation-like Function-like T-Sequence-like complex-valued set

p (#) x is Relation-like Function-like complex-valued set

dom x is epsilon-transitive epsilon-connected ordinal set

dom (p (#) x) is set

x is Relation-like Function-like complex-valued finite set

p is complex set

p + x is Relation-like Function-like complex-valued set

dom x is finite set

dom (p + x) is set

x - p is Relation-like Function-like complex-valued set

- p is complex set

(- p) + x is Relation-like Function-like complex-valued finite set

p (#) x is Relation-like Function-like complex-valued set

dom x is finite set

dom (p (#) x) is set

x is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

q is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

dom q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

p . y is set

y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(len x) - (y + 1) is ext-real complex real integer rational Element of INT

x . ((len x) - (y + 1)) is set

q . y is set

x is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

(x) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

dom (x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

rng x is finite set

rng (x) is finite set

len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

len (x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is set

q is set

x . q is set

y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(len x) -' (y + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(len x) - (y + 1) is ext-real complex real integer rational Element of INT

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(x) . r is set

r + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(len x) - (r + 1) is ext-real complex real integer rational Element of INT

x . ((len x) - (r + 1)) is set

p is set

q is set

(x) . q is set

y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

y + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(len x) -' (y + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(len x) - (y + 1) is ext-real complex real integer rational Element of INT

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(x) . y is set

x . ((len x) - (y + 1)) is set

x is set

p is Relation-like NAT -defined x -valued Function-like T-Sequence-like finite V86() set

(p) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

rng p is finite Element of K19(x)

K19(x) is set

rng (p) is finite set

x is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(len x) -' p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

y is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

dom y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

y . r is set

r + p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

x . (r + p) is set

q is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

dom q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

y is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

dom y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

q . r is set

r + p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

x . (r + p) is set

y . r is set

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(p,x) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

(len p) -' x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

len (p,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (p,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(p,x) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len (p,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (p,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(len p) - x is ext-real complex real Element of REAL

(len p) -' x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

x + p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

q is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(q,p) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

(q,p) . x is set

q . (x + p) is set

(len q) - p is ext-real complex real Element of REAL

len (q,p) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (q,p) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

dom (q,p) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

x is Relation-like NAT -defined Function-like one-to-one T-Sequence-like finite V86() set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(x,p) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

q is set

dom (x,p) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

y is set

(x,p) . q is set

(x,p) . y is set

dom (x,p) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

len (x,p) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(len x) -' p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

c

(len x) - p is ext-real complex real Element of REAL

r + p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

c

(x,p) . c

x . (c

(x,p) . r is set

x . (r + p) is set

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

(p,x) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

rng (p,x) is finite set

rng p is finite set

q is set

dom (p,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

y is set

(p,x) . y is set

len (p,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (p,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(len p) -' x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(len p) - x is ext-real complex real Element of REAL

r + x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

(p,x) . r is set

p . (r + x) is set

x is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

(x,0) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

len (x,0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (x,0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

dom (x,0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

(x,0) . p is set

p + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

x . (p + 0) is set

x . p is set

(len x) - 0 is ext-real non negative complex real integer rational Element of INT

len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(len p) + x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

q is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

p ^ q is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

((p ^ q),((len p) + x)) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

(q,x) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len (p ^ q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (p ^ q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

len q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(len p) + (len q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

len ((p ^ q),((len p) + x)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom ((p ^ q),((len p) + x)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(len (p ^ q)) - ((len p) + x) is ext-real complex real integer rational Element of INT

(len q) + (len p) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

((len q) + (len p)) - ((len p) + x) is ext-real complex real integer rational Element of INT

(len q) - x is ext-real complex real Element of REAL

len (q,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (q,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

dom (q,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

x + y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

dom ((p ^ q),((len p) + x)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

((p ^ q),((len p) + x)) . y is set

((len p) + x) + y is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(p ^ q) . (((len p) + x) + y) is set

(len p) + (x + y) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(p ^ q) . ((len p) + (x + y)) is set

q . (x + y) is set

(q,x) . y is set

x is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

x ^ p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

((x ^ p),(len x)) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

(len x) + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

((x ^ p),((len x) + 0)) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

(p,0) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

p | x is Relation-like x -defined NAT -defined rng p -valued Function-like T-Sequence-like finite V86() set

rng p is finite set

(p,x) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

(p | x) ^ (p,x) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p ^ {} is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

len (p | x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (p | x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

len (p,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (p,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(len p) - x is ext-real complex real Element of REAL

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

((p | x) ^ (p,x)) . r is set

(p | x) . r is set

p . r is set

r - x is ext-real complex real Element of REAL

max (0,(r - x)) is ext-real complex real set

c

dom (p,x) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

(len (p | x)) + c

((p | x) ^ (p,x)) . r is set

(p,x) . c

c

p . (c

p . r is set

((p | x) ^ (p,x)) . r is set

p . r is set

((p | x) ^ (p,x)) . r is set

p . r is set

len ((p | x) ^ (p,x)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom ((p | x) ^ (p,x)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

x + ((len p) - x) is ext-real complex real Element of REAL

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

x is set

p is Relation-like NAT -defined x -valued Function-like T-Sequence-like finite V86() set

q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(p,q) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(len p) - q is ext-real complex real Element of REAL

len (p,q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (p,q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

rng (p,q) is finite set

rng p is finite Element of K19(x)

K19(x) is set

c

dom (p,q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

c is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(p,q) . c is set

r + q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

c + q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of K19(NAT)

p . (c + q) is set

c

rng c

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

<%> x is Relation-like non-empty empty-yielding NAT -defined x -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V48() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V56() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V86() set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

x is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

x | q is Relation-like q -defined NAT -defined rng x -valued Function-like T-Sequence-like finite V86() set

rng x is finite set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

((x | q),(p -' 1)) is Relation-like NAT -defined rng x -valued Function-like T-Sequence-like finite V86() set

x is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(x,p,q) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

x | q is Relation-like q -defined NAT -defined rng x -valued Function-like T-Sequence-like finite V86() set

rng x is finite set

p -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

((x | q),(p -' 1)) is Relation-like NAT -defined rng x -valued Function-like T-Sequence-like finite V86() set

len (x | q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (x | q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

p - 1 is ext-real complex real Element of REAL

q + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(q + 1) - 1 is ext-real complex real integer rational Element of INT

x is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(x,(p -' 1)) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

q is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(x,p,q) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

x | q is Relation-like q -defined NAT -defined rng x -valued Function-like T-Sequence-like finite V86() set

rng x is finite set

((x | q),(p -' 1)) is Relation-like NAT -defined rng x -valued Function-like T-Sequence-like finite V86() set

q + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(q + 1) -' p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(x,(p -' 1)) | ((q + 1) -' p) is Relation-like (q + 1) -' p -defined NAT -defined rng (x,(p -' 1)) -valued Function-like T-Sequence-like finite V86() set

rng (x,(p -' 1)) is finite set

len (x | q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (x | q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

(p + 1) - 1 is ext-real complex real integer rational Element of INT

p - 1 is ext-real complex real Element of REAL

(q + 1) - p is ext-real complex real Element of REAL

q - (p - 1) is ext-real complex real Element of REAL

len (x,p,q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (x,p,q) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

len (x,(p -' 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom (x,(p -' 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(len x) - (p -' 1) is ext-real complex real integer rational Element of INT

c

(x,p,q) . c

((x,(p -' 1)) | ((q + 1) -' p)) . c

c

(q - (p - 1)) + (p -' 1) is ext-real complex real Element of REAL

c

((x | q),(p -' 1)) . c

(x | q) . (c

(x,(p -' 1)) . c

x . (c

len ((x,(p -' 1)) | ((q + 1) -' p)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom ((x,(p -' 1)) | ((q + 1) -' p)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

(p,1,x) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

p | x is Relation-like x -defined NAT -defined rng p -valued Function-like T-Sequence-like finite V86() set

rng p is finite set

1 -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

((p | x),(1 -' 1)) is Relation-like NAT -defined rng p -valued Function-like T-Sequence-like finite V86() set

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

len p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

dom p is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

(p,1,x) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

p | x is Relation-like x -defined NAT -defined rng p -valued Function-like T-Sequence-like finite V86() set

rng p is finite set

1 -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal Element of NAT

((p | x),(1 -' 1)) is Relation-like NAT -defined rng p -valued Function-like T-Sequence-like finite V86() set

x is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered cardinal set

p is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

(p,0,x) is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set

p | x is Relation-like x -defined NAT -defined rng p -valued Function-like T-Sequence-like finite V86() set

rng p is finite set

0 -' 1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural complex real integer finite rational complex-membered ext-real-membered real-membered rational-membered