:: INTEGRA3 semantic presentation

REAL is non empty V12() V37() V58() V59() V60() V64() non bounded_below non bounded_above interval set
NAT is non empty V12() epsilon-transitive epsilon-connected ordinal V37() cardinal limit_cardinal V58() V59() V60() V61() V62() V63() V64() left_end bounded_below Element of K19(REAL)
K19(REAL) is V12() V37() set
COMPLEX is non empty V12() V37() V58() V64() set
omega is non empty V12() epsilon-transitive epsilon-connected ordinal V37() cardinal limit_cardinal V58() V59() V60() V61() V62() V63() V64() left_end bounded_below set
K19(omega) is V12() V37() set
K19(NAT) is V12() V37() set
INT is non empty V12() V37() V58() V59() V60() V61() V62() V64() set
K164(NAT) is V36() set
{} is Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V37() V38() V41() cardinal {} -element FinSequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V58() V59() V60() V61() V62() V63() V64() bounded_below bounded_above real-bounded interval set
RAT is non empty V12() V37() V58() V59() V60() V61() V64() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
{{},1} is non empty V37() V41() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded set
K20(REAL,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is V12() V37() set
K20(COMPLEX,COMPLEX) is Relation-like V12() V37() complex-valued set
K19(K20(COMPLEX,COMPLEX)) is V12() V37() set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like V12() V37() complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() V37() set
K20(K20(REAL,REAL),REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is V12() V37() set
K20(RAT,RAT) is Relation-like RAT -valued V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is V12() V37() set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is V12() V37() set
K20(INT,INT) is Relation-like RAT -valued INT -valued V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is V12() V37() set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is V12() V37() set
K20(NAT,NAT) is Relation-like RAT -valued INT -valued V12() V37() complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V12() V37() complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is V12() V37() set
K333() is set
ExtREAL is non empty V59() interval set
K20(NAT,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is V12() V37() set
K20(COMPLEX,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(COMPLEX,REAL)) is V12() V37() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
0 is Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V37() V38() V41() cardinal {} -element FinSequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V58() V59() V60() V61() V62() V63() V64() V69() V70() bounded_below bounded_above real-bounded interval Element of NAT
Seg 1 is non empty V12() V37() 1 -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
{1} is non empty V12() V37() V41() 1 -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded set
Seg 2 is non empty V37() 2 -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
{1,2} is non empty V37() V41() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded set
A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
A -' A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
(A -' A) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
A - A is V22() real ext-real Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
chi (A,A) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is V12() V37() set
f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A
upper_volume ((chi (A,A)),f) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
sup (rng (upper_volume ((chi (A,A)),f))) is V22() real ext-real set
A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
divs A is non empty set
K20(NAT,(divs A)) is Relation-like V12() V37() set
K19(K20(NAT,(divs A))) is V12() V37() set
f is Relation-like Function-like non empty total V30( NAT , divs A) Element of K19(K20(NAT,(divs A)))
T is Relation-like Function-like non empty total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
e is Relation-like Function-like non empty total V30( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
T . e is V22() real ext-real Element of REAL
e . e is V22() real ext-real Element of REAL
f . e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A
(A,(f . e)) is V22() real ext-real Element of REAL
chi (A,A) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is V12() V37() set
upper_volume ((chi (A,A)),(f . e)) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng (upper_volume ((chi (A,A)),(f . e))) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
sup (rng (upper_volume ((chi (A,A)),(f . e)))) is V22() real ext-real set
A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A
(A,f) is V22() real ext-real Element of REAL
chi (A,A) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is V12() V37() set
upper_volume ((chi (A,A)),f) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
sup (rng (upper_volume ((chi (A,A)),f))) is V22() real ext-real set
T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A
(A,T) is V22() real ext-real Element of REAL
upper_volume ((chi (A,A)),T) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng (upper_volume ((chi (A,A)),T)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
sup (rng (upper_volume ((chi (A,A)),T))) is V22() real ext-real set
dom (upper_volume ((chi (A,A)),T)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
(upper_volume ((chi (A,A)),T)) . e is V22() real ext-real Element of REAL
len (upper_volume ((chi (A,A)),T)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom T is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
divset (T,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
vol (divset (T,e)) is V22() real ext-real Element of REAL
dom f is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
divset (f,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
vol (divset (f,e)) is V22() real ext-real Element of REAL
(upper_volume ((chi (A,A)),f)) . e is V22() real ext-real Element of REAL
len (upper_volume ((chi (A,A)),f)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
vol A is V22() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A
dom f is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
T is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
divset (f,T) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
vol (divset (f,T)) is V22() real ext-real Element of REAL
T is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
divset (f,T) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
upper_bound (divset (f,T)) is V22() real ext-real Element of REAL
lower_bound (divset (f,T)) is V22() real ext-real Element of REAL
vol (divset (f,T)) is V22() real ext-real Element of REAL
(upper_bound (divset (f,T))) - (lower_bound (divset (f,T))) is V22() real ext-real Element of REAL
(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len f) - 1 is V22() real ext-real Element of REAL
divset (f,(len f)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
upper_bound (divset (f,(len f))) is V22() real ext-real Element of REAL
f . (len f) is V22() real ext-real Element of REAL
lower_bound (divset (f,(len f))) is V22() real ext-real Element of REAL
f . ((len f) - 1) is V22() real ext-real Element of REAL
divset (f,(len f)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
upper_bound (divset (f,(len f))) is V22() real ext-real Element of REAL
f . (len f) is V22() real ext-real Element of REAL
upper_bound A is V22() real ext-real Element of REAL
lower_bound (divset (f,(len f))) is V22() real ext-real Element of REAL
lower_bound A is V22() real ext-real Element of REAL
(lower_bound A) + 0 is V22() real ext-real Element of REAL
(upper_bound A) - (lower_bound A) is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
f is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of f
dom T is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
lower_bound f is V22() real ext-real Element of REAL
upper_bound f is V22() real ext-real Element of REAL
rng T is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
T . e is V22() real ext-real Element of REAL
divset (T,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
lower_bound (divset (T,e)) is V22() real ext-real Element of REAL
upper_bound (divset (T,e)) is V22() real ext-real Element of REAL
e is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
lower_bound (divset (T,e)) is V22() real ext-real Element of REAL
upper_bound (divset (T,e)) is V22() real ext-real Element of REAL
e is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
divset (T,(len T)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
upper_bound (divset (T,(len T))) is V22() real ext-real Element of REAL
T . (len T) is V22() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal set
divset (T,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
upper_bound (divset (T,e)) is V22() real ext-real Element of REAL
divset (T,1) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
lower_bound (divset (T,1)) is V22() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal set
divset (T,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
lower_bound (divset (T,e)) is V22() real ext-real Element of REAL
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal set
divset (T,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
lower_bound (divset (T,e)) is V22() real ext-real Element of REAL
T . e is V22() real ext-real Element of REAL
e - 1 is V22() real ext-real Element of REAL
T . (e - 1) is V22() real ext-real Element of REAL
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
upper_bound (divset (T,e)) is V22() real ext-real Element of REAL
T . e is V22() real ext-real Element of REAL
e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
divset (T,(e + 1)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
lower_bound (divset (T,(e + 1))) is V22() real ext-real Element of REAL
(e + 1) - 1 is V22() real ext-real Element of REAL
T . ((e + 1) - 1) is V22() real ext-real Element of REAL
A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A
rng f is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A
rng T is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
(rng f) \/ (rng T) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
f ^ T is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng (f ^ T) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
card (rng (f ^ T)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of omega
e is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng e is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)
len e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
e is Relation-like NAT -defined REAL -valued Function-like one-to-one V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing FinSequence of REAL
y is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing FinSequence of REAL
rng y is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
len y is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
y . (len y) is V22() real ext-real Element of REAL
upper_bound A is V22() real ext-real Element of REAL
len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom f is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
f . (len f) is V22() real ext-real Element of REAL
dom y is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
y . D is V22() real ext-real Element of REAL
D is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A
rng D is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
card (rng f) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of omega
len D is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
card (rng T) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of omega
len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
chi (A,A) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is V12() V37() set
f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A
(A,f) is V22() real ext-real Element of REAL
upper_volume ((chi (A,A)),f) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
sup (rng (upper_volume ((chi (A,A)),f))) is V22() real ext-real set
dom f is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A
upper_volume ((chi (A,A)),T) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng (upper_volume ((chi (A,A)),T)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
inf (rng (upper_volume ((chi (A,A)),T))) is V22() real ext-real set
rng T is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
e is V22() real ext-real Element of REAL
e is V22() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
divset (f,y) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
(rng T) /\ (divset (f,y)) is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)
dom T is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
T . D is V22() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
T . p is V22() real ext-real Element of REAL
(T . D) - (T . p) is V22() real ext-real Element of REAL
abs ((T . D) - (T . p)) is V22() real ext-real Element of REAL
D + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len T) is non empty V37() len T -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
T . (D + 1) is V22() real ext-real Element of REAL
(T . D) - (T . (D + 1)) is V22() real ext-real Element of REAL
- ((T . D) - (T . (D + 1))) is V22() real ext-real Element of REAL
- ((T . D) - (T . p)) is V22() real ext-real Element of REAL
len (upper_volume ((chi (A,A)),T)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (A,A)),T))) is non empty V37() len (upper_volume ((chi (A,A)),T)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
dom (upper_volume ((chi (A,A)),T)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
(upper_volume ((chi (A,A)),T)) . (D + 1) is V22() real ext-real Element of REAL
divset (T,(D + 1)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
upper_bound (divset (T,(D + 1))) is V22() real ext-real Element of REAL
- (abs ((T . D) - (T . p))) is V22() real ext-real Element of REAL
lower_bound (divset (T,(D + 1))) is V22() real ext-real Element of REAL
(D + 1) - 1 is V22() real ext-real Element of REAL
T . ((D + 1) - 1) is V22() real ext-real Element of REAL
vol (divset (T,(D + 1))) is V22() real ext-real Element of REAL
(T . (D + 1)) - (T . D) is V22() real ext-real Element of REAL
p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len T) is non empty V37() len T -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
T . (p + 1) is V22() real ext-real Element of REAL
(T . (p + 1)) - (T . p) is V22() real ext-real Element of REAL
len (upper_volume ((chi (A,A)),T)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (A,A)),T))) is non empty V37() len (upper_volume ((chi (A,A)),T)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
dom (upper_volume ((chi (A,A)),T)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
(upper_volume ((chi (A,A)),T)) . (p + 1) is V22() real ext-real Element of REAL
divset (T,(p + 1)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
upper_bound (divset (T,(p + 1))) is V22() real ext-real Element of REAL
lower_bound (divset (T,(p + 1))) is V22() real ext-real Element of REAL
(p + 1) - 1 is V22() real ext-real Element of REAL
T . ((p + 1) - 1) is V22() real ext-real Element of REAL
vol (divset (T,(p + 1))) is V22() real ext-real Element of REAL
len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len f) is non empty V37() len f -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
len (upper_volume ((chi (A,A)),f)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (A,A)),f))) is non empty V37() len (upper_volume ((chi (A,A)),f)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
dom (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
(upper_volume ((chi (A,A)),f)) . y is V22() real ext-real Element of REAL
upper_bound (divset (f,y)) is V22() real ext-real Element of REAL
lower_bound (divset (f,y)) is V22() real ext-real Element of REAL
(T . p) - (lower_bound (divset (f,y))) is V22() real ext-real Element of REAL
(upper_bound (divset (f,y))) - (lower_bound (divset (f,y))) is V22() real ext-real Element of REAL
(T . p) - (T . D) is V22() real ext-real Element of REAL
vol (divset (f,y)) is V22() real ext-real Element of REAL
- ((T . D) - (T . p)) is V22() real ext-real Element of REAL
len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len f) is non empty V37() len f -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
len (upper_volume ((chi (A,A)),f)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (A,A)),f))) is non empty V37() len (upper_volume ((chi (A,A)),f)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
dom (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
(upper_volume ((chi (A,A)),f)) . y is V22() real ext-real Element of REAL
upper_bound (divset (f,y)) is V22() real ext-real Element of REAL
lower_bound (divset (f,y)) is V22() real ext-real Element of REAL
(T . D) - (lower_bound (divset (f,y))) is V22() real ext-real Element of REAL
(upper_bound (divset (f,y))) - (lower_bound (divset (f,y))) is V22() real ext-real Element of REAL
vol (divset (f,y)) is V22() real ext-real Element of REAL
A is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng A is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)
f is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng f is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)
len A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
T is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of T
dom e is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of T
indx (e,e,A) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
indx (e,e,f) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
dom e is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
e . A is V22() real ext-real Element of REAL
e . (indx (e,e,A)) is V22() real ext-real Element of REAL
e . f is V22() real ext-real Element of REAL
e . (indx (e,e,f)) is V22() real ext-real Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
T is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of T
dom e is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of T
indx (e,e,f) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
indx (e,e,A) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
e . A is V22() real ext-real Element of REAL
e . (indx (e,e,A)) is V22() real ext-real Element of REAL
dom e is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
e . f is V22() real ext-real Element of REAL
e . (indx (e,e,f)) is V22() real ext-real Element of REAL
A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of A
(A,f) is V22() real ext-real Element of REAL
chi (A,A) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is V12() V37() set
upper_volume ((chi (A,A)),f) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
sup (rng (upper_volume ((chi (A,A)),f))) is V22() real ext-real set
rng f is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
T is V22() real ext-real Element of REAL
dom f is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
f . e is V22() real ext-real Element of REAL
len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len f) is non empty V37() len f -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
len (upper_volume ((chi (A,A)),f)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (A,A)),f))) is non empty V37() len (upper_volume ((chi (A,A)),f)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
dom (upper_volume ((chi (A,A)),f)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
(upper_volume ((chi (A,A)),f)) . e is V22() real ext-real Element of REAL
divset (f,e) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
vol (divset (f,e)) is V22() real ext-real Element of REAL
A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is V12() V37() set
f is Relation-like Function-like non empty total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
f | A is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
rng f is non empty V58() V59() V60() Element of K19(REAL)
lower_bound (rng f) is V22() real ext-real Element of REAL
upper_bound (rng f) is V22() real ext-real Element of REAL
A is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(A,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is V12() V37() set
f is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
T is Relation-like Function-like non empty total V30(A, REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
T | A is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
rng T is non empty V58() V59() V60() Element of K19(REAL)
lower_bound (rng T) is V22() real ext-real Element of REAL
T | f is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
rng (T | f) is V58() V59() V60() Element of K19(REAL)
lower_bound (rng (T | f)) is V22() real ext-real Element of REAL
upper_bound (rng (T | f)) is V22() real ext-real Element of REAL
upper_bound (rng T) is V22() real ext-real Element of REAL
dom T is non empty set
dom (T | f) is set
e is V22() real ext-real Element of REAL
(T | f) . e is V22() real ext-real Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
f is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of f
dom T is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
divset (T,A) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
vol (divset (T,A)) is V22() real ext-real Element of REAL
(f,T) is V22() real ext-real Element of REAL
chi (f,f) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
K20(f,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is V12() V37() set
upper_volume ((chi (f,f)),T) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng (upper_volume ((chi (f,f)),T)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
sup (rng (upper_volume ((chi (f,f)),T))) is V22() real ext-real set
len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len T) is non empty V37() len T -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
len (upper_volume ((chi (f,f)),T)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (upper_volume ((chi (f,f)),T))) is non empty V37() len (upper_volume ((chi (f,f)),T)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
dom (upper_volume ((chi (f,f)),T)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
(upper_volume ((chi (f,f)),T)) . A is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
{A} is non empty V12() V37() 1 -element V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
f is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of f
len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(len T) - 1 is V22() real ext-real Element of REAL
divset (T,(len T)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
rng T is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
(rng T) \/ {A} is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of f
rng e is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
e is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
indx (e,T,e) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
e | (indx (e,T,e)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng (e | (indx (e,T,e))) is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)
T | e is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng (T | e) is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)
dom T is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
dom e is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
len e is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
lower_bound (divset (T,(len T))) is V22() real ext-real Element of REAL
T . e is V22() real ext-real Element of REAL
y is set
dom (e | (indx (e,T,e))) is V37() V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
(e | (indx (e,T,e))) . D is V22() real ext-real Element of REAL
len (e | (indx (e,T,e))) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
Seg (len (e | (indx (e,T,e)))) is V37() len (e | (indx (e,T,e))) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
Seg (indx (e,T,e)) is V37() indx (e,T,e) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
len (T | e) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
e . D is V22() real ext-real Element of REAL
e . (indx (e,T,e)) is V22() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
T . p is V22() real ext-real Element of REAL
Seg (len T) is non empty V37() len T -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
Seg e is V37() e -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
(T | e) . p is V22() real ext-real Element of REAL
dom (T | e) is V37() V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
dom (T | e) is V37() V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
(T | e) . e is V22() real ext-real Element of REAL
Seg e is V37() e -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
y is set
dom (T | e) is V37() V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
(T | e) . D is V22() real ext-real Element of REAL
len (T | e) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
Seg (len (T | e)) is V37() len (T | e) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
Seg e is V37() e -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
T . D is V22() real ext-real Element of REAL
indx (e,T,D) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
e . (indx (e,T,D)) is V22() real ext-real Element of REAL
e . (indx (e,T,e)) is V22() real ext-real Element of REAL
p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
e . p is V22() real ext-real Element of REAL
Seg (indx (e,T,e)) is V37() indx (e,T,e) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
len (e | (indx (e,T,e))) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
Seg (len (e | (indx (e,T,e)))) is V37() len (e | (indx (e,T,e))) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
dom (e | (indx (e,T,e))) is V37() V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
(e | (indx (e,T,e))) . p is V22() real ext-real Element of REAL
A is V22() real ext-real Element of REAL
{A} is non empty V12() V37() 1 -element V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
f is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
K20(f,REAL) is Relation-like V12() V37() complex-valued ext-real-valued real-valued set
K19(K20(f,REAL)) is V12() V37() set
T is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of f
len T is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
divset (T,(len T)) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
rng T is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
(rng T) \/ {A} is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
(f,T) is V22() real ext-real Element of REAL
chi (f,f) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
upper_volume ((chi (f,f)),T) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
rng (upper_volume ((chi (f,f)),T)) is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
sup (rng (upper_volume ((chi (f,f)),T))) is V22() real ext-real set
e is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing Division of f
rng e is non empty V37() V58() V59() V60() left_end right_end bounded_below bounded_above real-bounded Element of K19(REAL)
e is Relation-like Function-like non empty total V30(f, REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
e | f is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
lower_volume (e,e) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum (lower_volume (e,e)) is V22() real ext-real Element of REAL
K263() is Relation-like Function-like total V30(K20(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(K20(REAL,REAL),REAL))
K190(REAL,(lower_volume (e,e)),K263()) is V22() real ext-real Element of REAL
lower_volume (e,T) is Relation-like NAT -defined REAL -valued Function-like non empty V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum (lower_volume (e,T)) is V22() real ext-real Element of REAL
K190(REAL,(lower_volume (e,T)),K263()) is V22() real ext-real Element of REAL
(Sum (lower_volume (e,e))) - (Sum (lower_volume (e,T))) is V22() real ext-real Element of REAL
rng e is non empty V58() V59() V60() Element of K19(REAL)
upper_bound (rng e) is V22() real ext-real Element of REAL
lower_bound (rng e) is V22() real ext-real Element of REAL
(upper_bound (rng e)) - (lower_bound (rng e)) is V22() real ext-real Element of REAL
((upper_bound (rng e)) - (lower_bound (rng e))) * (f,T) is V22() real ext-real Element of REAL
dom T is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
indx (e,T,(len T)) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
dom e is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
(len T) - 1 is V22() real ext-real Element of REAL
D is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
mid (T,1,D) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
T | D is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
indx (e,T,D) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
mid (e,1,(indx (e,T,D))) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
e | (indx (e,T,D)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len e is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
len (e | (indx (e,T,D))) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
rng (e | (indx (e,T,D))) is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)
rng (T | D) is V37() V58() V59() V60() bounded_below bounded_above real-bounded Element of K19(REAL)
p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
indx (e,T,p) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
Seg (len e) is non empty V37() len e -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
Seg D is V37() D -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
Seg (indx (e,T,D)) is V37() indx (e,T,D) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
(e | (indx (e,T,D))) . (indx (e,T,p)) is V22() real ext-real Element of REAL
e . (indx (e,T,p)) is V22() real ext-real Element of REAL
T . p is V22() real ext-real Element of REAL
T . (indx (e,T,p)) is V22() real ext-real Element of REAL
Seg D is V37() D -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
T . p is V22() real ext-real Element of REAL
(T | D) . p is V22() real ext-real Element of REAL
e . (indx (e,T,p)) is V22() real ext-real Element of REAL
e . p is V22() real ext-real Element of REAL
Seg (indx (e,T,D)) is V37() indx (e,T,D) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
(lower_volume (e,T)) | D is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len ((lower_volume (e,T)) | D) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
(lower_volume (e,e)) | (indx (e,T,D)) is Relation-like NAT -defined REAL -valued Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Seg (len e) is non empty V37() len e -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
len (lower_volume (e,e)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
Seg (len (lower_volume (e,e))) is non empty V37() len (lower_volume (e,e)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
dom (lower_volume (e,e)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
p is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal set
((lower_volume (e,T)) | D) . p is V22() real ext-real Element of REAL
((lower_volume (e,e)) | (indx (e,T,D))) . p is V22() real ext-real Element of REAL
len (lower_volume (e,T)) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
H is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
Seg (len T) is non empty V37() len T -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
indx (e,T,H) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
Seg D is V37() D -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
Seg (indx (e,T,D)) is V37() indx (e,T,D) -element V58() V59() V60() V61() V62() V63() bounded_below bounded_above real-bounded Element of K19(NAT)
T . H is V22() real ext-real Element of REAL
e . (indx (e,T,H)) is V22() real ext-real Element of REAL
divset (T,H) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
lower_bound (divset (T,H)) is V22() real ext-real Element of REAL
divset (e,(indx (e,T,H))) is non empty V58() V59() V60() V100() closed_interval bounded_below bounded_above real-bounded interval Element of K19(REAL)
lower_bound (divset (e,(indx (e,T,H)))) is V22() real ext-real Element of REAL
upper_bound (divset (T,H)) is V22() real ext-real Element of REAL
upper_bound (divset (e,(indx (e,T,H)))) is V22() real ext-real Element of REAL
lower_bound f is V22() real ext-real Element of REAL
H - 1 is V22() real ext-real Element of REAL
h is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
H + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(indx (e,T,H)) - 1 is V22() real ext-real Element of REAL
e . ((indx (e,T,H)) - 1) is V22() real ext-real Element of REAL
T . (H - 1) is V22() real ext-real Element of REAL
e . (H - 1) is V22() real ext-real Element of REAL
indx (e,T,h) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V37() cardinal V58() V59() V60() V61() V62() V63() V69() V70() bounded_below bounded_above real-bounded Element of NAT
e . (indx (e,T,h)) is V22() real ext-real Element of REAL
[.(lower_bound (divset (T,H))),(upper_bound (divset (T,H))).] is V58() V59() V60() interval Element of K19(REAL)
Seg (len (lower_volume (e,T))) is non empty V37() len (lower_volume (e,T)) -element V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
dom (lower_volume (e,T)) is non empty V37() V58() V59() V60() V61() V62() V63() left_end right_end bounded_below bounded_above real-bounded Element of K19(NAT)
((lower_volume (e,T)) | D) . H is V22() real ext-real Element of REAL
(lower_volume (e,T)) . H is V22() real ext-real Element of REAL
e | (divset (e,(indx (e,T,H)))) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K19(K20(f,REAL))
rng (e | (divset (e,(indx (e,T,H))))) is V58() V59() V60() Element of K19(REAL)
lower_bound (rng (e | (divset (e,(indx (e,T,H)))))) is V22() real ext-real Element of REAL
vol (divset (e,(indx (e,T,H)))) is V22() real ext-real Element of REAL
(lower_bound (rng (e | (divset (e,(indx (e,T,H))))))) * (vol (divset (e,(indx (e,T,H))))) is V22() real ext-real Element of REAL
((lower_volume (e,e)) | (indx (e,T,D))) . H is V22() real ext-real Element of REAL
((lower_v