:: SEQM_3 semantic presentation

REAL is non empty V47() V48() V49() V53() V54() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() V54() V65() V66() Element of K19(REAL)
K19(REAL) is V54() 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 V33() real complex-valued ext-real-valued real-valued natural-valued V47() V48() V49() V50() V51() V52() V53() V54() bounded_above bounded_below V65() V67( {} ) FinSequence-like FinSubsequence-like FinSequence-membered bounded set
RAT is non empty V47() V48() V49() V50() V53() V54() set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
{{},1} is non empty V47() V48() V49() V50() V51() V52() set
COMPLEX is non empty V47() V53() V54() set
INT is non empty V47() V48() V49() V50() V51() V53() V54() set
omega is non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() V54() V65() V66() set
K19(omega) is V54() set
K19(NAT) is V54() set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
K20(NAT,REAL) is Relation-like complex-valued ext-real-valued real-valued V54() set
K19(K20(NAT,REAL)) is V54() set
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 V33() real V35() V36() complex-valued ext-real-valued real-valued natural-valued V47() V48() V49() V50() V51() V52() V53() V54() bounded_above bounded_below V65() V67( {} ) FinSequence-like FinSubsequence-like FinSequence-membered bounded Element of NAT
K20(NAT,NAT) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued V54() set
K19(K20(NAT,NAT)) is V54() set
Seg 1 is non empty V12() V47() V48() V49() V50() V51() V52() V54() V67(1) Element of K19(NAT)
{1} is non empty V12() V47() V48() V49() V50() V51() V52() V67(1) set
Seg 2 is non empty V47() V48() V49() V50() V51() V52() V54() V67(2) Element of K19(NAT)
{1,2} is non empty V47() V48() V49() V50() V51() V52() set
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V54() V65() set
v + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V54() V65() set
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v + 1) + i is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + 1) + m is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((n + 1) + m) is ext-real V33() real Element of REAL
((n + 1) + m) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (((n + 1) + m) + 1) is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + 1) + (m + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((n + 1) + (m + 1)) is ext-real V33() real Element of REAL
(n + 1) + 0 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((n + 1) + 0) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + 1) + k is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + 1) + m is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((n + 1) + m) is ext-real V33() real Element of REAL
((n + 1) + m) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (((n + 1) + m) + 1) is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + 1) + (m + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((n + 1) + (m + 1)) is ext-real V33() real Element of REAL
(n + 1) + 0 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((n + 1) + 0) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + 1) + k is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + m) is ext-real V33() real Element of REAL
(n + m) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((n + m) + 1) is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + (m + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + (m + 1)) is ext-real V33() real Element of REAL
n + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 0) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V54() V65() set
n + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + m) is ext-real V33() real Element of REAL
(n + m) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((n + m) + 1) is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + (m + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + (m + 1)) is ext-real V33() real Element of REAL
n + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 0) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V54() V65() set
n + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued set
dom v is V47() V48() V49() V50() V51() V52() set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
n is ext-real set
v . n is ext-real V33() real set
m is ext-real set
v . m is ext-real V33() real set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
v . m is ext-real V33() real Element of REAL
n is ext-real set
v . n is ext-real V33() real set
m is ext-real set
v . m is ext-real V33() real set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
v . m is ext-real V33() real Element of REAL
n is ext-real set
v . n is ext-real V33() real set
m is ext-real set
v . m is ext-real V33() real set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
n is ext-real set
v . n is ext-real V33() real set
m is ext-real set
v . m is ext-real V33() real set
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
dom v is non empty V47() V48() V49() V50() V51() V52() set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is non empty V47() V48() V49() V50() V51() V52() set
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + 1) + k is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
dom v is non empty V47() V48() V49() V50() V51() V52() set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is non empty V47() V48() V49() V50() V51() V52() set
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + 1) + k is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
dom v is non empty V47() V48() V49() V50() V51() V52() set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is non empty V47() V48() V49() V50() V51() V52() set
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V54() V65() set
n + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
dom v is non empty V47() V48() V49() V50() V51() V52() set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is non empty V47() V48() V49() V50() V51() V52() set
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V54() V65() set
n + k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + 1) + m is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((n + 1) + m) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is non empty V47() V48() V49() V50() V51() V52() set
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + 1) + m is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((n + 1) + m) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + 1) + m is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((n + 1) + m) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is non empty V47() V48() V49() V50() V51() V52() set
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + 1) + m is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((n + 1) + m) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
v . m is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is non empty V47() V48() V49() V50() V51() V52() set
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + m) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + m) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
v . m is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is non empty V47() V48() V49() V50() V51() V52() set
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + m) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + m) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is non empty V47() V48() V49() V50() V51() V52() set
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
v . 0 is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . 0 is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v . 0 is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
v . 0 is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is V47() V48() V49() V50() V51() V52() set
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is V47() V48() V49() V50() V51() V52() set
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is set
dom v is V47() V48() V49() V50() V51() V52() set
v . n is ext-real V33() real set
m is set
v . m is ext-real V33() real set
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . k is ext-real V33() real Element of REAL
v . i is ext-real V33() real Element of REAL
incl NAT is Relation-like NAT -defined REAL -valued NAT -valued RAT -valued INT -valued Function-like one-to-one non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(incl NAT) . n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V54() V65() Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(incl NAT) . (n + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V54() V65() Element of REAL
id NAT is Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like one-to-one non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
v is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(NAT,NAT))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (m + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n . (k + 1) is ext-real V33() real Element of REAL
n . k is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng v is non empty V47() V48() V49() set
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
dom v is non empty V47() V48() V49() V50() V51() V52() set
rng v is non empty V47() V48() V49() set
n is set
dom v is non empty V47() V48() V49() V50() V51() V52() set
m is set
v . m is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . k is ext-real V33() real Element of REAL
v is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v ^\ n is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued subsequence of v
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(m + n) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((m + n) + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (m + n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(m + 1) + n is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . ((m + 1) + n) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v ^\ n) . m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v ^\ n) . (m + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is Relation-like Function-like ext-real-valued set
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real V33() real Element of REAL
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real V33() real Element of REAL
v . n is ext-real V33() real Element of REAL
v is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (n + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V54() V65() set
v ^\ n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of v
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n
m is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n + m is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n + m) ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n + m
m ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of m
(n ^\ v) + (m ^\ v) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
((n + m) ^\ v) . k is ext-real V33() real Element of REAL
k + v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n + m) . (k + v) is ext-real V33() real Element of REAL
n . (k + v) is ext-real V33() real Element of REAL
m . (k + v) is ext-real V33() real Element of REAL
(n . (k + v)) + (m . (k + v)) is ext-real V33() real Element of REAL
(n ^\ v) . k is ext-real V33() real Element of REAL
((n ^\ v) . k) + (m . (k + v)) is ext-real V33() real Element of REAL
(m ^\ v) . k is ext-real V33() real Element of REAL
((n ^\ v) . k) + ((m ^\ v) . k) is ext-real V33() real Element of REAL
((n ^\ v) + (m ^\ v)) . k is ext-real V33() real Element of REAL
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
K137(1) is ext-real non positive V33() real set
K137(1) (#) n is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- n) ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of - n
n ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n
- (n ^\ v) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
K137(1) (#) (n ^\ v) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
((- n) ^\ v) . m is ext-real V33() real Element of REAL
m + v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(- n) . (m + v) is ext-real V33() real Element of REAL
n . (m + v) is ext-real V33() real Element of REAL
- (n . (m + v)) is ext-real V33() real Element of REAL
(n ^\ v) . m is ext-real V33() real Element of REAL
- ((n ^\ v) . m) is ext-real V33() real Element of REAL
(- (n ^\ v)) . m is ext-real V33() real Element of REAL
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n
m is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n - m is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- m is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
K137(1) is ext-real non positive V33() real set
K137(1) (#) m is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n + (- m) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(n - m) ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n - m
m ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of m
(n ^\ v) - (m ^\ v) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (m ^\ v) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
K137(1) (#) (m ^\ v) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(n ^\ v) + (- (m ^\ v)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
- m is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- m) ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of - m
(n ^\ v) + ((- m) ^\ v) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n ") ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n "
n ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n
(n ^\ v) " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
((n ") ^\ v) . m is ext-real V33() real Element of REAL
m + v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n ") . (m + v) is ext-real V33() real Element of REAL
n . (m + v) is ext-real V33() real Element of REAL
(n . (m + v)) " is ext-real V33() real Element of REAL
(n ^\ v) . m is ext-real V33() real Element of REAL
((n ^\ v) . m) " is ext-real V33() real Element of REAL
((n ^\ v) ") . m is ext-real V33() real Element of REAL
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n
m is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n (#) m is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n (#) m) ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n (#) m
m ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of m
(n ^\ v) (#) (m ^\ v) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
((n (#) m) ^\ v) . k is ext-real V33() real Element of REAL
k + v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n (#) m) . (k + v) is ext-real V33() real Element of REAL
n . (k + v) is ext-real V33() real Element of REAL
m . (k + v) is ext-real V33() real Element of REAL
(n . (k + v)) * (m . (k + v)) is ext-real V33() real Element of REAL
(n ^\ v) . k is ext-real V33() real Element of REAL
((n ^\ v) . k) * (m . (k + v)) is ext-real V33() real Element of REAL
(m ^\ v) . k is ext-real V33() real Element of REAL
((n ^\ v) . k) * ((m ^\ v) . k) is ext-real V33() real Element of REAL
((n ^\ v) (#) (m ^\ v)) . k is ext-real V33() real Element of REAL
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n
m is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n /" m is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
n (#) (m ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(n /" m) ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n /" m
m ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of m
(n ^\ v) /" (m ^\ v) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(m ^\ v) " is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(n ^\ v) (#) ((m ^\ v) ") is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
m " is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(m ") ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of m "
(n ^\ v) (#) ((m ") ^\ v) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is ext-real V33() real set
m is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n (#) m is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(n (#) m) ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of n (#) m
m ^\ v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of m
n (#) (m ^\ v) is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
((n (#) m) ^\ v) . k is ext-real V33() real Element of REAL
k + v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(n (#) m) . (k + v) is ext-real V33() real Element of REAL
m . (k + v) is ext-real V33() real Element of REAL
n * (m . (k + v)) is ext-real V33() real Element of REAL
(m ^\ v) . k is ext-real V33() real Element of REAL
n * ((m ^\ v) . k) is ext-real V33() real Element of REAL
(n (#) (m ^\ v)) . k is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
k is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
v * k is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of v
k . (m + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k . m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (k . (m + 1)) is ext-real V33() real Element of REAL
v . (k . m) is ext-real V33() real Element of REAL
(v * k) . m is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n . (m + 1) is ext-real V33() real Element of REAL
k is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
v * k is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of v
k . (m + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k . m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (k . m) is ext-real V33() real Element of REAL
v . (k . (m + 1)) is ext-real V33() real Element of REAL
(v * k) . (m + 1) is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n . (m + 1) is ext-real V33() real Element of REAL
k is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
v * k is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of v
k . m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k . (m + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (k . m) is ext-real V33() real Element of REAL
v . (k . (m + 1)) is ext-real V33() real Element of REAL
(v * k) . m is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
k is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
v * k is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of v
k . m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k . (m + 1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (k . (m + 1)) is ext-real V33() real Element of REAL
v . (k . m) is ext-real V33() real Element of REAL
(v * k) . (m + 1) is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real V33() real set
k is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
v * k is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of v
i is ext-real V33() real set
r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n . r is ext-real V33() real Element of REAL
n . r is ext-real V33() real Element of REAL
k . r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (k . r) is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real V33() real set
k is Relation-like NAT -defined NAT -valued Function-like non empty total V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
v * k is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of v
i is ext-real V33() real set
r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n . r is ext-real V33() real Element of REAL
n . r is ext-real V33() real Element of REAL
k . r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (k . r) is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . (m + 1) is ext-real V33() real Element of REAL
(v (#) n) . m is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
v * (n . (m + 1)) is ext-real V33() real Element of REAL
v * (n . m) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V54() V65() set
n . m is ext-real V33() real Element of REAL
v * (n . m) is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n . (m + 1) is ext-real V33() real Element of REAL
v * (n . (m + 1)) is ext-real V33() real Element of REAL
(v (#) n) . m is ext-real V33() real Element of REAL
(v (#) n) . (m + 1) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . (m + 1) is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
v * (n . m) is ext-real V33() real Element of REAL
v * (n . (m + 1)) is ext-real V33() real Element of REAL
v is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
v * (n . m) is ext-real V33() real Element of REAL
v * (n . (m + 1)) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . (m + 1) is ext-real V33() real Element of REAL
(v (#) n) . m is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
v * (n . (m + 1)) is ext-real V33() real Element of REAL
v * (n . m) is ext-real V33() real Element of REAL
v is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
v * (n . m) is ext-real V33() real Element of REAL
v * (n . (m + 1)) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . (m + 1) is ext-real V33() real Element of REAL
(v (#) n) . m is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
v * (n . (m + 1)) is ext-real V33() real Element of REAL
v * (n . m) is ext-real V33() real Element of REAL
v is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . (m + 1) is ext-real V33() real Element of REAL
(v (#) n) . m is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
v * (n . (m + 1)) is ext-real V33() real Element of REAL
v * (n . m) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . (m + 1) is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
v * (n . m) is ext-real V33() real Element of REAL
v * (n . (m + 1)) is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v + n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v + n) . (m + 1) is ext-real V33() real Element of REAL
(v + n) . m is ext-real V33() real Element of REAL
v . (m + 1) is ext-real V33() real Element of REAL
v . m is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
(v . (m + 1)) + (n . (m + 1)) is ext-real V33() real Element of REAL
(v . m) + (n . m) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v + n) . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v + n) . (m + 1) is ext-real V33() real Element of REAL
v . m is ext-real V33() real Element of REAL
v . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
(v . m) + (n . m) is ext-real V33() real Element of REAL
(v . (m + 1)) + (n . (m + 1)) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v + n) . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v + n) . (m + 1) is ext-real V33() real Element of REAL
v . m is ext-real V33() real Element of REAL
v . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
(v . m) + (n . m) is ext-real V33() real Element of REAL
(v . (m + 1)) + (n . (m + 1)) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v + n) . (m + 1) is ext-real V33() real Element of REAL
(v + n) . m is ext-real V33() real Element of REAL
v . (m + 1) is ext-real V33() real Element of REAL
v . m is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
(v . (m + 1)) + (n . (m + 1)) is ext-real V33() real Element of REAL
(v . m) + (n . m) is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v + n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v + n) . (m + 1) is ext-real V33() real Element of REAL
(v + n) . m is ext-real V33() real Element of REAL
k is ext-real V33() real Element of REAL
v . (m + 1) is ext-real V33() real Element of REAL
v . m is ext-real V33() real Element of REAL
(v . (m + 1)) + k is ext-real V33() real Element of REAL
(v . m) + k is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
(v . m) + (n . m) is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
(v . (m + 1)) + (n . (m + 1)) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v + n) . m is ext-real V33() real Element of REAL
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v + n) . (m + 1) is ext-real V33() real Element of REAL
k is ext-real V33() real Element of REAL
v . m is ext-real V33() real Element of REAL
v . (m + 1) is ext-real V33() real Element of REAL
(v . m) + k is ext-real V33() real Element of REAL
(v . (m + 1)) + k is ext-real V33() real Element of REAL
n . (m + 1) is ext-real V33() real Element of REAL
(v . (m + 1)) + (n . (m + 1)) is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
(v . m) + (n . m) is ext-real V33() real Element of REAL
v is ext-real V33() real set
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v (#) n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . m is ext-real V33() real Element of REAL
n . m is ext-real V33() real Element of REAL
0 * (n . m) is ext-real V33() real Element of REAL
- 1 is ext-real non positive V33() real Element of REAL
m is ext-real non positive V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . k is ext-real V33() real Element of REAL
n . k is ext-real V33() real Element of REAL
v * (n . k) is ext-real V33() real Element of REAL
(v (#) n) . k is ext-real V33() real Element of REAL
m is ext-real V33() real set
abs m is ext-real V33() real Element of REAL
v * (abs m) is ext-real V33() real Element of REAL
k is ext-real V33() real Element of REAL
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v (#) n) . i is ext-real V33() real Element of REAL
n . i is ext-real V33() real Element of REAL
v * (n . i) is ext-real V33() real Element of REAL
(v (#) n) . i is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
K137(1) is ext-real non positive V33() real set
K137(1) (#) v is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
abs v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued bounded_below Element of K19(K20(NAT,REAL))
n is ext-real V33() real set
n (#) v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is ext-real V33() real set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(abs v) . m is ext-real V33() real Element of REAL
abs ((abs v) . m) is ext-real V33() real Element of REAL
v . m is ext-real V33() real Element of REAL
abs (v . m) is ext-real V33() real Element of REAL
abs (abs (v . m)) is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v + n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real V33() real set
n . 0 is ext-real V33() real Element of REAL
m + (n . 0) is ext-real V33() real Element of REAL
k is ext-real V33() real Element of REAL
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v + n) . i is ext-real V33() real Element of REAL
n . i is ext-real V33() real Element of REAL
v . i is ext-real V33() real Element of REAL
(v . i) + (n . i) is ext-real V33() real Element of REAL
(v + n) . i is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
v + n is Relation-like NAT -defined REAL -valued Function-like non empty total V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
m is ext-real V33() real set
n . 0 is ext-real V33() real Element of REAL
m + (n . 0) is ext-real V33() real Element of REAL
k is ext-real V33() real Element of REAL
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(v + n) . i is ext-real V33() real Element of REAL
n . i is ext-real V33() real Element of REAL
v . i is ext-real V33() real Element of REAL
(v . i) + (n . i) is ext-real V33() real Element of REAL
(v + n) . i is ext-real V33() real Element of REAL
v is Relation-like NAT -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued V54() FinSequence-like FinSubsequence-like FinSequence of NAT
v is ext-real V33() real Element of REAL
v + 1 is ext-real V33() real Element of REAL
n is ext-real V33() real Element of REAL
v - n is ext-real V33() real Element of REAL
abs (v - n) is ext-real V33() real Element of REAL
n + 1 is ext-real V33() real Element of REAL
n - v is ext-real V33() real Element of REAL
- (v - n) is ext-real V33() real Element of REAL
abs (- (v - n)) is ext-real V33() real Element of REAL
- (v - n) is ext-real V33() real Element of REAL
abs (- (v - n)) is ext-real V33() real Element of REAL
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v - n is ext-real V33() real Element of REAL
abs (v - n) is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m - k is ext-real V33() real Element of REAL
abs (m - k) is ext-real V33() real Element of REAL
(abs (v - n)) + (abs (m - k)) is ext-real V33() real Element of REAL
(abs (v - n)) + 0 is ext-real V33() real Element of REAL
k - m is ext-real V33() real Element of REAL
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
- (k - m) is ext-real V33() real Element of REAL
abs (- (k - m)) is ext-real V33() real Element of REAL
abs i is ext-real V33() real V36() Element of REAL
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V54() V65() set
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
n + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v is Relation-like NAT -defined Function-like V54() FinSequence-like FinSubsequence-like set
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is V47() V48() V49() V50() V51() V52() Element of K19(NAT)
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
Del (v,n) is Relation-like NAT -defined Function-like V54() FinSequence-like FinSubsequence-like set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
Seg m is V47() V48() V49() V50() V51() V52() V54() V67(m) Element of K19(NAT)
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(Del (v,n)) . k is set
v . k is set
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (k + 1) is set
{n} is non empty V12() V47() V48() V49() V50() V51() V52() V67(1) set
(dom v) \ {n} is V47() V48() V49() V50() V51() V52() Element of K19(NAT)
Seg (len v) is V47() V48() V49() V50() V51() V52() V54() V67( len v) Element of K19(NAT)
Sgm ((dom v) \ {n}) is Relation-like NAT -defined NAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued V54() FinSequence-like FinSubsequence-like FinSequence of NAT
(Sgm ((dom v) \ {n})) . k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V54() V65() Element of REAL
rng (Sgm ((dom v) \ {n})) is V47() V48() V49() V50() V51() V52() set
(Sgm ((dom v) \ {n})) (#) v is Relation-like NAT -defined Function-like set
dom ((Sgm ((dom v) \ {n})) (#) v) is V47() V48() V49() V50() V51() V52() set
dom (Sgm ((dom v) \ {n})) is V47() V48() V49() V50() V51() V52() Element of K19(NAT)
len (Sgm ((dom v) \ {n})) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
Seg (len (Sgm ((dom v) \ {n}))) is V47() V48() V49() V50() V51() V52() V54() V67( len (Sgm ((dom v) \ {n}))) Element of K19(NAT)
v is Relation-like NAT -defined Function-like V54() FinSequence-like FinSubsequence-like set
dom v is V47() V48() V49() V50() V51() V52() Element of K19(NAT)
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . n is set
v . m is set
n is set
dom v is V47() V48() V49() V50() V51() V52() set
m is set
v . n is set
v . m is set
v is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V54() FinSequence-like FinSubsequence-like FinSequence of REAL
<*0*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing V54() bounded_above bounded_below V67(1) FinSequence-like FinSubsequence-like bounded FinSequence of REAL
v is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing V54() bounded_above bounded_below V67(1) FinSequence-like FinSubsequence-like bounded FinSequence of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v is non empty V12() V47() V48() V49() V50() V51() V52() V67(1) set
v . n is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
dom v is non empty V12() V47() V48() V49() V50() V51() V52() V67(1) Element of K19(NAT)
<*0*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty V12() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V54() bounded_above bounded_below V67(1) FinSequence-like FinSubsequence-like bounded FinSequence of NAT
dom <*0*> is non empty V12() V47() V48() V49() V50() V51() V52() V67(1) Element of K19(NAT)
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -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 V33() real complex-valued ext-real-valued real-valued natural-valued non-decreasing non-increasing V47() V48() V49() V50() V51() V52() V53() V54() bounded_above bounded_below V65() V67( {} ) FinSequence-like FinSubsequence-like FinSequence-membered bounded FinSequence of REAL
v is Relation-like non-empty empty-yielding NAT -defined REAL -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 V33() real complex-valued ext-real-valued real-valued natural-valued non-decreasing non-increasing V47() V48() V49() V50() V51() V52() V53() V54() bounded_above bounded_below V65() V67( {} ) FinSequence-like FinSubsequence-like FinSequence-membered bounded FinSequence of REAL
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
dom v 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 V33() real complex-valued ext-real-valued real-valued natural-valued V47() V48() V49() V50() V51() V52() V53() V54() bounded_above bounded_below V65() V67( {} ) FinSequence-like FinSubsequence-like FinSequence-membered bounded Element of K19(NAT)
v . n 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 V33() real complex-valued ext-real-valued real-valued natural-valued V47() V48() V49() V50() V51() V52() V53() V54() bounded_above bounded_below V65() V67( {} ) FinSequence-like FinSubsequence-like FinSequence-membered bounded set
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m 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 V33() real complex-valued ext-real-valued real-valued natural-valued V47() V48() V49() V50() V51() V52() V53() V54() bounded_above bounded_below V65() V67( {} ) FinSequence-like FinSubsequence-like FinSequence-membered bounded set
v is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V54() FinSequence-like FinSubsequence-like FinSequence of REAL
rng v is V47() V48() V49() set
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (len v) is ext-real V33() real Element of REAL
(len v) - 1 is ext-real V33() real Element of REAL
dom v is V47() V48() V49() V50() V51() V52() Element of K19(NAT)
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
Seg n is V47() V48() V49() V50() V51() V52() V54() V67(n) Element of K19(NAT)
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . k is ext-real V33() real Element of REAL
k + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (k + 1) is ext-real V33() real Element of REAL
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
i is ext-real V33() real Element of REAL
m - i is ext-real V33() real Element of REAL
abs (m - i) is ext-real V33() real Element of REAL
i + 1 is ext-real V33() real Element of REAL
r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
r + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k + l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (k + l) is ext-real V33() real Element of REAL
j is ext-real V33() real Element of REAL
k + r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(k + r) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k + (r + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (k + r) is ext-real V33() real Element of REAL
s is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
s - j is ext-real V33() real Element of REAL
abs (s - j) is ext-real V33() real Element of REAL
j + 1 is ext-real V33() real Element of REAL
s + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k - k is ext-real V33() real Element of REAL
j + 1 is ext-real V33() real Element of REAL
s + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
s - j is ext-real V33() real Element of REAL
abs (s - j) is ext-real V33() real Element of REAL
(len v) - k is ext-real V33() real Element of REAL
r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k + r is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k + l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
j is ext-real V33() real Element of REAL
v . (k + l) is ext-real V33() real Element of REAL
i + 1 is ext-real V33() real Element of REAL
i + 1 is ext-real V33() real Element of REAL
i is ext-real V33() real Element of REAL
k - k is ext-real V33() real Element of REAL
i is ext-real V33() real Element of REAL
m - i is ext-real V33() real Element of REAL
abs (m - i) is ext-real V33() real Element of REAL
i is ext-real V33() real Element of REAL
m - i is ext-real V33() real Element of REAL
abs (m - i) is ext-real V33() real Element of REAL
v is Relation-like NAT -defined REAL -valued Function-like complex-valued ext-real-valued real-valued V54() FinSequence-like FinSubsequence-like FinSequence of REAL
rng v is V47() V48() V49() set
v . 1 is ext-real V33() real Element of REAL
len v is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (len v) is ext-real V33() real Element of REAL
(len v) - 1 is ext-real V33() real Element of REAL
dom v is V47() V48() V49() V50() V51() V52() Element of K19(NAT)
n is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
Seg n is V47() V48() V49() V50() V51() V52() V54() V67(n) Element of K19(NAT)
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
k is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . k is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V54() V65() set
v . k is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . k is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V54() V65() set
v . k is ext-real V33() real Element of REAL
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . i is ext-real V33() real Element of REAL
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
i + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
r is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . r is ext-real V33() real Element of REAL
k is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . k is ext-real V33() real Element of REAL
m is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . m is ext-real V33() real Element of REAL
k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . k is ext-real V33() real Element of REAL
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
r is ext-real V33() real Element of REAL
i + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (m + 1) is ext-real V33() real Element of REAL
l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
l + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (m + j) is ext-real V33() real Element of REAL
s is ext-real V33() real Element of REAL
m + l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + (l + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
(m + l) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
v . (m + l) is ext-real V33() real Element of REAL
r1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
r1 - s is ext-real V33() real Element of REAL
abs (r1 - s) is ext-real V33() real Element of REAL
s + 1 is ext-real V33() real Element of REAL
s1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m - m is ext-real V33() real Element of REAL
r1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
s + 1 is ext-real V33() real Element of REAL
r1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
r1 - s is ext-real V33() real Element of REAL
abs (r1 - s) is ext-real V33() real Element of REAL
k - m is ext-real V33() real Element of REAL
l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + l is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
m + j is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V33() real V35() V36() V47() V48() V49() V50() V51() V52() V54() V65() Element of NAT
s is ext-real V33() real Element of REAL
v . (m + j) is ext-real V33() real Element of REAL