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)
c6 is finite set
q .: c6 is finite Element of K19(p)
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 c6 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 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)
c6 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
c6 -' 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
c6 + 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
(c6 + 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
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
(c6 + 1) - 1 is ext-real complex real integer rational Element of INT
r . c6 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 . c6) + 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
max (c,((r . c6) + 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
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
(c6 + 1) - 1 is ext-real complex real integer rational Element of INT
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
(c6 + 1) - 1 is ext-real complex real integer rational Element of INT
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
c6 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 . c6 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
(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
c6 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 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
F2() is non empty set
F1() 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
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
F3(q) is Element of F2()
p is Relation-like NAT -defined F2() -valued 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
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
F3(q) is Element of F2()
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
c6 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 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)
c6 + 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) . c6 is set
x . (c6 + p) is set
(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
c6 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 Element of K19(NAT)
(len (p | x)) + c6 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) ^ (p,x)) . r is set
(p,x) . c6 is set
c6 + 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
p . (c6 + x) is set
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
c6 is set
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
c6 is Relation-like NAT -defined Function-like T-Sequence-like finite V86() set
rng c6 is finite 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 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
c6 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) . c6 is set
((x,(p -' 1)) | ((q + 1) -' p)) . c6 is set
c6 + (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
(q - (p - 1)) + (p -' 1) is ext-real complex real Element of REAL
c6 + (p - 1) is ext-real complex real Element of REAL
((x | q),(p -' 1)) . c6 is set
(x | q) . (c6 + (p -' 1)) is set
(x,(p -' 1)) . c6 is set
x . (c6 + (p -' 1)) is set
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