:: RFINSEQ2 semantic presentation

REAL is non empty V12() V38() V59() V60() V61() V65() set
NAT is V12() V25() V38() cardinal limit_cardinal V59() V60() V61() V62() V63() V64() V65() Element of K19(REAL)
K19(REAL) is V12() V38() set
COMPLEX is non empty V12() V38() V59() V65() set
RAT is non empty V12() V38() V59() V60() V61() V62() V65() set
INT is non empty V12() V38() V59() V60() V61() V62() V63() V65() set
K20(COMPLEX,COMPLEX) is V12() V38() V49() set
K19(K20(COMPLEX,COMPLEX)) is V12() V38() set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V12() V38() V49() set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() V38() set
K20(REAL,REAL) is V12() V38() V49() V50() V51() set
K19(K20(REAL,REAL)) is V12() V38() set
K20(K20(REAL,REAL),REAL) is V12() V38() V49() V50() V51() set
K19(K20(K20(REAL,REAL),REAL)) is V12() V38() set
K20(RAT,RAT) is RAT -valued V12() V38() V49() V50() V51() set
K19(K20(RAT,RAT)) is V12() V38() set
K20(K20(RAT,RAT),RAT) is RAT -valued V12() V38() V49() V50() V51() set
K19(K20(K20(RAT,RAT),RAT)) is V12() V38() set
K20(INT,INT) is RAT -valued INT -valued V12() V38() V49() V50() V51() set
K19(K20(INT,INT)) is V12() V38() set
K20(K20(INT,INT),INT) is RAT -valued INT -valued V12() V38() V49() V50() V51() set
K19(K20(K20(INT,INT),INT)) is V12() V38() set
K20(NAT,NAT) is RAT -valued INT -valued V49() V50() V51() V52() set
K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued V49() V50() V51() V52() set
K19(K20(K20(NAT,NAT),NAT)) is set
NAT is V12() V25() V38() cardinal limit_cardinal V59() V60() V61() V62() V63() V64() V65() set
K19(NAT) is V12() V38() set
K19(NAT) is V12() V38() set
ExtREAL is non empty V60() set
K20(NAT,REAL) is V12() V38() V49() V50() V51() set
K19(K20(NAT,REAL)) is V12() V38() set
{} is Function-like functional empty V25() V29() ext-real non positive non negative V38() V42() cardinal {} -element FinSequence-membered V59() V60() V61() V62() V63() V64() V65() set
1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
2 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
3 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
Seg 1 is non empty V12() V38() 1 -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
{1} is non empty V12() V38() V42() 1 -element V59() V60() V61() V62() V63() V64() set
Seg 2 is non empty V38() 2 -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
{1,2} is non empty V38() V42() V59() V60() V61() V62() V63() V64() set
0 is Function-like functional empty V25() V29() V30() V31() ext-real non positive non negative V35() V36() V38() V42() cardinal {} -element FinSequence-membered V59() V60() V61() V62() V63() V64() V65() Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
Seg (len f) is V38() len f -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r1 is V30() V31() ext-real Element of REAL
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r1 is V30() V31() ext-real Element of REAL
f . 1 is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
i is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
0 + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
i is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
i is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
i is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . i is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
r2 is V30() V31() ext-real Element of REAL
r3 is V30() V31() ext-real Element of REAL
i is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . i is V30() V31() ext-real Element of REAL
1 + j is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
i is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . i is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
i is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . i is V30() V31() ext-real Element of REAL
f . 1 is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 is V30() V31() ext-real Element of REAL
f . j is V30() V31() ext-real Element of REAL
r2 is V30() V31() ext-real Element of REAL
i is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . i is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r1 is V30() V31() ext-real Element of REAL
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r1 is V30() V31() ext-real Element of REAL
r2 is V30() V31() ext-real Element of REAL
i is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r1 is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
Seg (len f) is V38() len f -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r1 is V30() V31() ext-real Element of REAL
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r1 is V30() V31() ext-real Element of REAL
f . 1 is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
i is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
0 + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
i is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
i is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
i is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . i is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
r2 is V30() V31() ext-real Element of REAL
r3 is V30() V31() ext-real Element of REAL
i is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . i is V30() V31() ext-real Element of REAL
1 + j is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
i is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . i is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
i is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . i is V30() V31() ext-real Element of REAL
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
i is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . i is V30() V31() ext-real Element of REAL
f . 1 is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 is V30() V31() ext-real Element of REAL
f . j is V30() V31() ext-real Element of REAL
r2 is V30() V31() ext-real Element of REAL
i is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . i is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r1 is V30() V31() ext-real Element of REAL
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r1 is V30() V31() ext-real Element of REAL
r2 is V30() V31() ext-real Element of REAL
i is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r1 is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r1 is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
(f) is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
(f) is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) is V30() V31() ext-real Element of REAL
f . (f) is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
<*j*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() V38() 1 -element FinSequence-like FinSubsequence-like V49() V50() V51() V53() V54() V55() non-increasing FinSequence of REAL
f . 1 is V30() V31() ext-real Element of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) is V30() V31() ext-real Element of REAL
f . (f) is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
<*j*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() V38() 1 -element FinSequence-like FinSubsequence-like V49() V50() V51() V53() V54() V55() non-increasing FinSequence of REAL
f . 1 is V30() V31() ext-real Element of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
r1 is V30() V31() ext-real Element of REAL
<*j,r1*> is Relation-like NAT -defined Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like set
max (j,r1) is ext-real set
IFEQ (j,(max (j,r1)),1,2) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . 2 is V30() V31() ext-real Element of REAL
f . 1 is V30() V31() ext-real Element of REAL
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
1 + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
r1 is V30() V31() ext-real Element of REAL
<*j,r1*> is Relation-like NAT -defined Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like set
min (j,r1) is ext-real set
IFEQ (j,(min (j,r1)),1,2) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . 1 is V30() V31() ext-real Element of REAL
f . 2 is V30() V31() ext-real Element of REAL
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
1 + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f + j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
((f + j)) is V30() V31() ext-real Element of REAL
((f + j)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f + j) . ((f + j)) is V30() V31() ext-real Element of REAL
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
(j) is V30() V31() ext-real Element of REAL
(j) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j . (j) is V30() V31() ext-real Element of REAL
(f) + (j) is V30() V31() ext-real Element of REAL
len (f + j) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom (f + j) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
Seg (len f) is V38() len f -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom j is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
j . ((f + j)) is V30() V31() ext-real Element of REAL
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f . ((f + j)) is V30() V31() ext-real Element of REAL
(f . ((f + j))) + (j . ((f + j))) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
(j) is V30() V31() ext-real Element of REAL
(j) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j . (j) is V30() V31() ext-real Element of REAL
(f) + (j) is V30() V31() ext-real Element of REAL
f + j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
((f + j)) is V30() V31() ext-real Element of REAL
((f + j)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f + j) . ((f + j)) is V30() V31() ext-real Element of REAL
len (f + j) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom (f + j) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
Seg (len f) is V38() len f -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom j is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
j . ((f + j)) is V30() V31() ext-real Element of REAL
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f . ((f + j)) is V30() V31() ext-real Element of REAL
(f . ((f + j))) + (j . ((f + j))) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
j * f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
((j * f)) is V30() V31() ext-real Element of REAL
((j * f)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(j * f) . ((j * f)) is V30() V31() ext-real Element of REAL
j * (f) is V30() V31() ext-real Element of REAL
len (j * f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom (j * f) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
Seg (len f) is V38() len f -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f . ((j * f)) is V30() V31() ext-real Element of REAL
j * (f . ((j * f))) is V30() V31() ext-real Element of REAL
j * (f . (f)) is V30() V31() ext-real Element of REAL
(j * f) . (f) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
j is V30() V31() ext-real Element of REAL
j * f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
((j * f)) is V30() V31() ext-real Element of REAL
((j * f)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(j * f) . ((j * f)) is V30() V31() ext-real Element of REAL
j * (f) is V30() V31() ext-real Element of REAL
len (j * f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom (j * f) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f . ((j * f)) is V30() V31() ext-real Element of REAL
j * (f . (f)) is V30() V31() ext-real Element of REAL
j * (f . ((j * f))) is V30() V31() ext-real Element of REAL
(j * f) . (f) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
((- f)) is V30() V31() ext-real Element of REAL
((- f)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(- f) . ((- f)) is V30() V31() ext-real Element of REAL
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
- (f) is V30() V31() ext-real Element of REAL
len (- f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom (- f) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
Seg (len f) is V38() len f -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f . ((- f)) is V30() V31() ext-real Element of REAL
- (f . ((- f))) is V30() V31() ext-real Element of REAL
- (f . (f)) is V30() V31() ext-real Element of REAL
(- f) . (f) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
((- f)) is V30() V31() ext-real Element of REAL
((- f)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(- f) . ((- f)) is V30() V31() ext-real Element of REAL
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
- (f) is V30() V31() ext-real Element of REAL
len (- f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom (- f) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
Seg (len f) is V38() len f -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f . ((- f)) is V30() V31() ext-real Element of REAL
- (f . (f)) is V30() V31() ext-real Element of REAL
- (f . ((- f))) is V30() V31() ext-real Element of REAL
(- f) . (f) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f /^ j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
((f /^ j)) is V30() V31() ext-real Element of REAL
((f /^ j)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f /^ j) . ((f /^ j)) is V30() V31() ext-real Element of REAL
((f /^ j)) is V30() V31() ext-real Element of REAL
((f /^ j)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f /^ j) . ((f /^ j)) is V30() V31() ext-real Element of REAL
1 + j is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
len (f /^ j) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(len f) - j is V30() V31() ext-real Element of REAL
dom (f /^ j) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
((f /^ j)) + j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (((f /^ j)) + j) is V30() V31() ext-real Element of REAL
((len f) - j) + j is V30() V31() ext-real Element of REAL
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
((f /^ j)) + j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (((f /^ j)) + j) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
(j) is V30() V31() ext-real Element of REAL
(j) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j . (j) is V30() V31() ext-real Element of REAL
dom j is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
K20((dom j),(dom j)) is RAT -valued INT -valued V38() V49() V50() V51() V52() set
K19(K20((dom j),(dom j))) is V38() V42() set
r1 is Relation-like dom j -defined dom j -valued Function-like one-to-one V14( dom j) quasi_total onto bijective V38() V49() V50() V51() V52() Element of K19(K20((dom j),(dom j)))
r1 * j is Relation-like Function-like V38() V49() V50() V51() set
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom (r1 * j) is V38() set
(r1 * j) . (f) is V30() V31() ext-real Element of REAL
r1 . (f) is V25() V29() V30() V31() ext-real non negative V38() cardinal Element of REAL
j . (r1 . (f)) is V30() V31() ext-real Element of REAL
Seg (len j) is V38() len j -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom r1 is V38() set
rng r1 is V38() V59() V60() V61() V62() V63() V64() Element of K19(REAL)
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
(j) is V30() V31() ext-real Element of REAL
(j) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j . (j) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(j) is V30() V31() ext-real Element of REAL
(j) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j . (j) is V30() V31() ext-real Element of REAL
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
dom j is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
K20((dom j),(dom j)) is RAT -valued INT -valued V38() V49() V50() V51() V52() set
K19(K20((dom j),(dom j))) is V38() V42() set
r1 is Relation-like dom j -defined dom j -valued Function-like one-to-one V14( dom j) quasi_total onto bijective V38() V49() V50() V51() V52() Element of K19(K20((dom j),(dom j)))
r1 * j is Relation-like Function-like V38() V49() V50() V51() set
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
Seg (len j) is V38() len j -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom r1 is V38() set
dom (r1 * j) is V38() set
(r1 * j) . (f) is V30() V31() ext-real Element of REAL
r1 . (f) is V25() V29() V30() V31() ext-real non negative V38() cardinal Element of REAL
j . (r1 . (f)) is V30() V31() ext-real Element of REAL
rng r1 is V38() V59() V60() V61() V62() V63() V64() Element of K19(REAL)
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
(j) is V30() V31() ext-real Element of REAL
(j) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j . (j) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
r1 is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
r1 is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
<*> REAL is Relation-like NAT -defined REAL -valued Function-like one-to-one constant functional empty V25() V29() ext-real non positive non negative V38() V39() V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() V50() V51() V52() V59() V60() V61() V62() V63() V64() V65() FinSequence of REAL
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
j + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (j + 1) is V30() V31() ext-real Element of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r1 is V30() V31() ext-real Element of REAL
f . 0 is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
f . r1 is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . j is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (len f) is V30() V31() ext-real Element of REAL
j . (len j) is V30() V31() ext-real Element of REAL
r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f | r1 is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
j | r1 is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
f . (r1 + 1) is V30() V31() ext-real Element of REAL
j . (r1 + 1) is V30() V31() ext-real Element of REAL
0 + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
<*(f . (r1 + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() V38() 1 -element FinSequence-like FinSubsequence-like V49() V50() V51() V53() V54() V55() non-increasing FinSequence of REAL
(f | r1) ^ <*(f . (r1 + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
dom j is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
rng f is V38() V59() V60() V61() Element of K19(REAL)
rng j is V38() V59() V60() V61() Element of K19(REAL)
j is V25() V29() ext-real non negative V38() cardinal set
f . j is V30() V31() ext-real Element of REAL
j is V25() V29() ext-real non negative V38() cardinal set
j . j is V30() V31() ext-real Element of REAL
(j | r1) ^ <*(f . (r1 + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
j is set
{j} is non empty V12() V38() 1 -element set
(f | r1) " {j} is V38() set
card ((f | r1) " {j}) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
<*(f . (r1 + 1))*> " {j} is V38() set
card (<*(f . (r1 + 1))*> " {j}) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(card ((f | r1) " {j})) + (card (<*(f . (r1 + 1))*> " {j})) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
Coim (f,j) is V38() set
f " {j} is V38() set
card (Coim (f,j)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
Coim (j,j) is V38() set
j " {j} is V38() set
card (Coim (j,j)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(j | r1) " {j} is V38() set
card ((j | r1) " {j}) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(card ((j | r1) " {j})) + (card (<*(f . (r1 + 1))*> " {j})) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
Coim ((f | r1),j) is V38() set
card (Coim ((f | r1),j)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
Coim ((j | r1),j) is V38() set
card (Coim ((j | r1),j)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f | j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len (f | j) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
0 + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
len (f | j) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom (f | j) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
Seg (len (f | j)) is V38() len (f | j) -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
r2 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r2 + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . r2 is V30() V31() ext-real Element of REAL
(f | j) . r2 is V30() V31() ext-real Element of REAL
f . (r2 + 1) is V30() V31() ext-real Element of REAL
(f | j) . (r2 + 1) is V30() V31() ext-real Element of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
j . (f + 1) is V30() V31() ext-real Element of REAL
j | f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
r1 | f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len r1 is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j . (len j) is V30() V31() ext-real Element of REAL
r1 . (len r1) is V30() V31() ext-real Element of REAL
<*(j . (f + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V12() V38() 1 -element FinSequence-like FinSubsequence-like V49() V50() V51() V53() V54() V55() non-increasing FinSequence of REAL
(j | f) ^ <*(j . (f + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len (j | f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
i is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
<*> REAL is Relation-like NAT -defined REAL -valued Function-like one-to-one constant functional empty V25() V29() ext-real non positive non negative V38() V39() V42() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() V50() V51() V52() V59() V60() V61() V62() V63() V64() V65() FinSequence of REAL
f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
r1 is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
r1 is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
(f) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
(f) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
- f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
dom (- f) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(- f) . j is V30() V31() ext-real Element of REAL
(- f) . (j + 1) is V30() V31() ext-real Element of REAL
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f . j is V30() V31() ext-real Element of REAL
- (f . j) is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
- (f . (j + 1)) is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
- f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
dom (- f) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
j + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(- f) . (j + 1) is V30() V31() ext-real Element of REAL
(- f) . j is V30() V31() ext-real Element of REAL
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f . j is V30() V31() ext-real Element of REAL
- (f . j) is V30() V31() ext-real Element of REAL
f . (j + 1) is V30() V31() ext-real Element of REAL
- (f . (j + 1)) is V30() V31() ext-real Element of REAL
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
dom j is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
K20((dom j),(dom j)) is RAT -valued INT -valued V38() V49() V50() V51() V52() set
K19(K20((dom j),(dom j))) is V38() V42() set
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
- j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
r1 is Relation-like dom j -defined dom j -valued Function-like one-to-one V14( dom j) quasi_total onto bijective V38() V49() V50() V51() V52() Element of K19(K20((dom j),(dom j)))
r1 * j is Relation-like Function-like V38() V49() V50() V51() set
r1 * (- j) is Relation-like Function-like V38() V49() V50() V51() set
rng r1 is V38() V59() V60() V61() V62() V63() V64() Element of K19(REAL)
dom (- j) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
rng (r1 * (- j)) is V38() V59() V60() V61() Element of K19(REAL)
rng (- j) is V38() V59() V60() V61() Element of K19(REAL)
dom (- f) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom (r1 * j) is V38() set
dom r1 is V38() set
dom (r1 * (- j)) is V38() set
Seg (len j) is V38() len j -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
r2 is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
i is V25() V29() ext-real non negative V38() cardinal set
(- f) . i is V30() V31() ext-real Element of REAL
r2 . i is V30() V31() ext-real Element of REAL
r1 . i is V25() V29() V30() V31() ext-real non negative V38() cardinal Element of REAL
f . i is V30() V31() ext-real Element of REAL
- (f . i) is V30() V31() ext-real Element of REAL
j . (r1 . i) is V30() V31() ext-real Element of REAL
- (j . (r1 . i)) is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(- j) . j is V30() V31() ext-real Element of REAL
(r1 * (- j)) . i is V30() V31() ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
- f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
- j is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
dom j is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
K20((dom j),(dom j)) is RAT -valued INT -valued V38() V49() V50() V51() V52() set
K19(K20((dom j),(dom j))) is V38() V42() set
r1 is Relation-like dom j -defined dom j -valued Function-like one-to-one V14( dom j) quasi_total onto bijective V38() V49() V50() V51() V52() Element of K19(K20((dom j),(dom j)))
r1 * j is Relation-like Function-like V38() V49() V50() V51() set
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 * (- j) is Relation-like Function-like V38() V49() V50() V51() set
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
0 + 1 is non empty V25() V29() V30() V31() ext-real positive non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
len (- f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 * (- j) is Relation-like Function-like V38() V49() V50() V51() set
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 * (- j) is Relation-like Function-like V38() V49() V50() V51() set
len j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 * (- j) is Relation-like Function-like V38() V49() V50() V51() set
dom (- j) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
- f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
((- f)) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
(f) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
- (f) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
- (- f) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
- ((- f)) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
- f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
((- f)) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
(f) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
- (f) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
- (- f) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
- ((- f)) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(f) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
dom (f) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
len (f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
(f) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
dom (f) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom f is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
len (f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() FinSequence of REAL
len f is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-increasing FinSequence of REAL
((f)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) is Relation-like NAT -defined REAL -valued Function-like V38() FinSequence-like FinSubsequence-like V49() V50() V51() non-decreasing FinSequence of REAL
((f)) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) . 1 is V30() V31() ext-real Element of REAL
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
(f) . 1 is V30() V31() ext-real Element of REAL
(f) is V30() V31() ext-real Element of REAL
(f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . (f) is V30() V31() ext-real Element of REAL
len (f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
Seg (len (f)) is V38() len (f) -element V59() V60() V61() V62() V63() V64() Element of K19(NAT)
dom (f) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) . j is V30() V31() ext-real Element of REAL
r1 is V30() V31() ext-real Element of REAL
r2 is V30() V31() ext-real Element of REAL
len (f) is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom (f) is V38() V59() V60() V61() V62() V63() V64() Element of K19(NAT)
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) . j is V30() V31() ext-real Element of REAL
r1 is V30() V31() ext-real Element of REAL
r2 is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) . j is V30() V31() ext-real Element of REAL
((f)) is V30() V31() ext-real Element of REAL
(f) . ((f)) is V30() V31() ext-real Element of REAL
j is V25() V29() V30() V31() ext-real non negative V35() V36() V38() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(f) . j is V30() V31() ext-real Element of REAL
((f)) is V30() V31() ext-real Element of REAL
(f) . ((f)) is V30() V31() ext-real Element of REAL